# HG changeset patch
# User skalberg
# Date 1058801243 -7200
# Node ID 433f9a4145378ebbbcf43ac9cfc9368545e9abb5
# Parent  d2a0fd183f5fc6e0a0c51d012f836f6e2d05a395
Added handling of meta implication and meta quantification.

diff -r d2a0fd183f5f -r 433f9a414537 src/HOL/Tools/specification_package.ML
--- a/src/HOL/Tools/specification_package.ML	Mon Jul 21 16:19:34 2003 +0200
+++ b/src/HOL/Tools/specification_package.ML	Mon Jul 21 17:27:23 2003 +0200
@@ -90,7 +90,8 @@
 		Type.typ_instance(tsig,t,u) andalso
 		Type.typ_instance(tsig,u,t)
 	    end
-	val prop = term_of (Thm.read_cterm sg (sprop,HOLogic.boolT))
+	val cprop = Thm.read_cterm sg (sprop,Term.propT)
+	val prop = term_of cprop
 	val (prop_thawed,vmap) = Type.varify (prop,[])
 	val thawed_prop_consts = collect_consts (prop_thawed,[])
 	val (altcos,overloaded) = Library.split_list cos
@@ -110,11 +111,14 @@
 		  | [cf] => unvarify cf vmap
 		  | _ => error ("Several variations of \"" ^ (Sign.string_of_term sg c) ^ "\" found in specification")
 	    end
-	val frees = Term.term_frees prop
+	val rew_imp = Simplifier.full_rewrite (empty_ss setmksimps single addsimps [thm "HOL.atomize_imp",thm "HOL.atomize_all"]) cprop
+	val cprop' = snd (dest_equals (cprop_of rew_imp))
+	val prop' = HOLogic.dest_Trueprop (term_of cprop')
+	val frees = Term.term_frees prop'
 	val tsig = Sign.tsig_of (sign_of thy)
 	val _ = assert (forall (fn v => Type.of_sort tsig (type_of v,HOLogic.typeS)) frees)
 		"Only free variables of sort 'type' allowed in specifications"
-	val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) (map dest_Free frees,prop)
+	val prop_closed = foldr (fn ((vname,T),prop) => HOLogic.mk_all (vname,T,prop)) (map dest_Free frees,prop')
 	val proc_consts = map proc_const consts
 	fun mk_exist (c,prop) =
 	    let
@@ -145,8 +149,12 @@
 		    end
 		fun remove_alls frees thm = foldl (inst_all (sign_of_thm thm)) (thm,frees)
 		fun apply_atts arg = Thm.apply_attributes (arg,map (Attrib.global_attribute thy) atts)
+		fun undo_imps thm =
+		    equal_elim (symmetric rew_imp) thm
 	    in
-		arg |> apsnd (remove_alls frees)
+		arg |> apsnd freezeT
+		    |> apsnd (remove_alls frees)
+		    |> apsnd (undo_imps)
 		    |> apsnd standard
 		    |> apply_atts
 		    |> add_final