# HG changeset patch
# User wenzelm
# Date 1206814446 -3600
# Node ID 28dd7c7a9a2efa945dbe8542e4b6cc2760a8c6e9
# Parent  b8f62618ad0ac25ac4f56f9520749b7bec1bba2d
eliminated non-linear access to thy1 and thy12c;

diff -r b8f62618ad0a -r 28dd7c7a9a2e src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 29 19:14:05 2008 +0100
+++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Mar 29 19:14:06 2008 +0100
@@ -56,7 +56,6 @@
   let val T = fastype_of x
   in Const ("List.list.Cons", T --> HOLogic.listT T --> HOLogic.listT T) $ x $ xs end;
 
-
 (* this function sets up all matters related to atom-  *)
 (* kinds; the user specifies a list of atom-kind names *)
 (* atom_decl <ak1> ... <akn>                           *)
@@ -118,7 +117,7 @@
                                           simp_tac (HOL_basic_ss addsimps simp3) 1]  
            
               val (inf_thm,thy4) =  
-                    PureThy.add_thms [((ak^"_infinite",Goal.prove_global thy1 [] [] stmnt3 proof3), [])] thy3
+                    PureThy.add_thms [((ak^"_infinite",Goal.prove_global thy3 [] [] stmnt3 proof3), [])] thy3
           in 
             ((inj_thm,inject_thm,inf_thm),thy4)
           end) ak_names thy
@@ -469,7 +468,7 @@
            thy'
            |> AxClass.prove_arity (qu_name,[],[cls_name])
               (if ak_name = ak_name' then proof1 else proof2)
-         end) ak_names thy) ak_names thy12c;
+         end) ak_names thy) ak_names thy12d;
 
      (* show that                       *)
      (*      fun(pt_<ak>,pt_<ak>)       *)