# [isabelle] can anyone explain this?

```
IN the attached theory file, (also copied below),
I get an error at

lemmas bin_nth_simps = bin_nth_0 bin_nth_Suc ;

the error being

*** Unknown theorem(s) "bin_nth_0"
```
*** At command "lemmas" (line 40 of "/home/users/jeremy/isabelle/l4/bg.thy").
```
However when I delete the earlier line

lemmas fs = funpow_Suc ;

then this error does not occur.

Does anyone know why this might be?

Thanks for any help

Jeremy

PS this is with Isabelle_11-Feb-2007

file bg.thy follows

theory bg imports Main

begin

consts
(* corresponding operations analysing bins *)
bin_nth :: "int => nat => bool"

primrec
Z : "bin_nth w 0 = True"
Suc : "bin_nth w (Suc n) = False"

ML {*
use_legacy_bindings (the_context()) ;
*}

ML {*
val _ = ListPair.app bind_thm (["funpow_0", "funpow_Suc"],
thms "funpow.simps") ;
*}

(* if this is deleted then bin_nth_0 below is recognised
*)
lemmas fs = funpow_Suc ;

ML {*
```
val _ = ListPair.app bind_thm (["bin_nth_0", "bin_nth_Suc"], bin_nth.simps) ;
```  *}

lemmas bin_nth_simps = bin_nth_0 bin_nth_Suc ;

end

```
```(*
ID:         \$Id: BinGeneral.thy 2667 2006-09-26 07:15:00Z gklein \$
Author:     Jeremy Dawson, NICTA

*)

theory bg imports Main

begin

consts
(* corresponding operations analysing bins *)
bin_nth :: "int => nat => bool"

primrec
Z : "bin_nth w 0 = True"
Suc : "bin_nth w (Suc n) = False"

ML {*
use_legacy_bindings (the_context()) ;
*}

ML {*
val _ = ListPair.app bind_thm (["funpow_0", "funpow_Suc"],
thms "funpow.simps") ;
*}

(* if this is deleted then bin_nth_0 below is recognised
lemmas fs = funpow_Suc ;
*)

ML {*
val _ = ListPair.app bind_thm (["bin_nth_0", "bin_nth_Suc"], bin_nth.simps) ;
*}

lemmas bin_nth_simps = bin_nth_0 bin_nth_Suc ;

end

```

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.