src/HOL/Nominal/nominal_atoms.ML
changeset 26484 28dd7c7a9a2e
parent 26398 fccb74555d9e
child 26773 ba8b1a8a12a7
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 29 19:14:05 2008 +0100
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 29 19:14:06 2008 +0100
     1.3 @@ -56,7 +56,6 @@
     1.4    let val T = fastype_of x
     1.5    in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
     1.6  
     1.7 -
     1.8  (* this function sets up all matters related to atom-  *)
     1.9  (* kinds; the user specifies a list of atom-kind names *)
    1.10  (* atom_decl <ak1> ... <akn>                           *)
    1.11 @@ -118,7 +117,7 @@
    1.12                                            simp_tac (HOL_basic_ss addsimps simp3) 1]  
    1.13             
    1.14                val (inf_thm,thy4) =  
    1.15 -                    PureThy.add_thms [((ak^"_infinite",Goal.prove_global thy1 [] [] stmnt3 proof3), [])] thy3
    1.16 +                    PureThy.add_thms [((ak^"_infinite",Goal.prove_global thy3 [] [] stmnt3 proof3), [])] thy3
    1.17            in 
    1.18              ((inj_thm,inject_thm,inf_thm),thy4)
    1.19            end) ak_names thy
    1.20 @@ -469,7 +468,7 @@
    1.21             thy'
    1.22             |> AxClass.prove_arity (qu_name,[],[cls_name])
    1.23                (if ak_name = ak_name' then proof1 else proof2)
    1.24 -         end) ak_names thy) ak_names thy12c;
    1.25 +         end) ak_names thy) ak_names thy12d;
    1.26  
    1.27       (* show that                       *)
    1.28       (*      fun(pt_<ak>,pt_<ak>)       *)