src/HOL/Nominal/nominal_atoms.ML
changeset 20046 9c8909fc5865
parent 19993 e0a5783d708f
child 20097 be2d96bbf39c
     1.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 08 12:54:32 2006 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Sat Jul 08 12:54:33 2006 +0200
     1.3 @@ -175,7 +175,7 @@
     1.4          val proof = fn _ => auto_tac (claset(),simp_s);
     1.5  
     1.6        in 
     1.7 -        ((name, standard (Goal.prove thy5 [] [] statement proof)), []) 
     1.8 +        ((name, Goal.prove_global thy5 [] [] statement proof), []) 
     1.9        end) ak_names_types);
    1.10  
    1.11      (* declares a perm-axclass for every atom-kind               *)
    1.12 @@ -236,7 +236,7 @@
    1.13  
    1.14          val proof = fn _ => auto_tac (claset(),simp_s);
    1.15        in 
    1.16 -        ((name, standard (Goal.prove thy7 [] [] statement proof)), []) 
    1.17 +        ((name, Goal.prove_global thy7 [] [] statement proof), []) 
    1.18        end) ak_names_types);
    1.19  
    1.20       (* declares an fs-axclass for every atom-kind       *)
    1.21 @@ -281,7 +281,7 @@
    1.22  
    1.23           val proof = fn _ => auto_tac (claset(),simp_s);
    1.24         in 
    1.25 -         ((name, standard (Goal.prove thy11 [] [] statement proof)), []) 
    1.26 +         ((name, Goal.prove_global thy11 [] [] statement proof), []) 
    1.27         end) ak_names_types);
    1.28  
    1.29         (* declares for every atom-kind combination an axclass            *)
    1.30 @@ -332,7 +332,7 @@
    1.31  
    1.32               val proof = fn _ => EVERY [auto_tac (claset(),simp_s), rtac cp1 1];
    1.33  	   in
    1.34 -	     PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy'
    1.35 +	     PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
    1.36  	   end) 
    1.37             ak_names_types thy) ak_names_types thy12b;
    1.38         
    1.39 @@ -363,7 +363,7 @@
    1.40  
    1.41                   val proof = fn _ => auto_tac (claset(),simp_s);
    1.42  	       in
    1.43 -		PureThy.add_thms [((name, standard (Goal.prove thy' [] [] statement proof)), [])] thy'
    1.44 +		PureThy.add_thms [((name, Goal.prove_global thy' [] [] statement proof), [])] thy'
    1.45  	       end
    1.46             else 
    1.47              ([],thy')))  (* do nothing branch, if ak_name = ak_name' *)