# HG changeset patch
# User wenzelm
# Date 1213281714 -7200
# Node ID c2c484480f404ee653d47c860e86999d89d41e2d
# Parent  9ae98c3cd3d63468143ba5d9ded316df36a1c1bf
declare_skofuns/skolem: canonical argument order;
minor tuning;

diff -r 9ae98c3cd3d6 -r c2c484480f40 src/HOL/Tools/res_axioms.ML
--- a/src/HOL/Tools/res_axioms.ML	Thu Jun 12 16:41:47 2008 +0200
+++ b/src/HOL/Tools/res_axioms.ML	Thu Jun 12 16:41:54 2008 +0200
@@ -68,42 +68,40 @@
   in fold (#2 #> Term.fold_atyps add_new_TFrees) rhs_consts [] end;
 
 (*Traverse a theorem, declaring Skolem function definitions. String s is the suggested
-  prefix for the Skolem constant. Result is a new theory*)
-fun declare_skofuns s th thy =
-  let val nref = ref 0
-      fun dec_sko (Const ("Ex",_) $ (xtp as Abs(_,T,p))) (thy, axs) =
-            (*Existential: declare a Skolem function, then insert into body and continue*)
-            let val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
-                val args0 = term_frees xtp  (*get the formal parameter list*)
-                val Ts = map type_of args0
-                val extraTs = rhs_extra_types (Ts ---> T) xtp
-                val _ = if null extraTs then () else
-                   warning ("Skolemization: extra type vars: " ^
-                            commas_quote (map (Syntax.string_of_typ_global thy) extraTs));
-                val argsx = map (fn T => Free(gensym"vsk", T)) extraTs
-                val args = argsx @ args0
-                val cT = extraTs ---> Ts ---> T
-                val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
-                        (*Forms a lambda-abstraction over the formal parameters*)
-                val _ = Output.debug (fn () => "declaring the constant " ^ cname)
-                val (c, thy') =
-                  Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy
-                           (*Theory is augmented with the constant, then its def*)
-                val cdef = cname ^ "_def"
-                val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy'
-                            handle ERROR _ => raise Clausify_failure thy'
-            in dec_sko (subst_bound (list_comb(c,args), p))
-                               (thy'', Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef) :: axs)
-            end
-        | dec_sko (Const ("All",_) $ (xtp as Abs(a,T,p))) thx =
-            (*Universal quant: insert a free variable into body and continue*)
-            let val fname = Name.variant (add_term_names (p,[])) a
-            in dec_sko (subst_bound (Free(fname,T), p)) thx end
-        | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
-        | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
-        | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
-        | dec_sko t thx = thx (*Do nothing otherwise*)
-  in  dec_sko (prop_of th) (thy,[])  end;
+  prefix for the Skolem constant.*)
+fun declare_skofuns s th =
+  let
+    val nref = ref 0
+    fun dec_sko (Const ("Ex",_) $ (xtp as Abs (_, T, p))) (axs, thy) =
+          (*Existential: declare a Skolem function, then insert into body and continue*)
+          let
+            val cname = "sko_" ^ s ^ "_" ^ Int.toString (inc nref)
+            val args0 = term_frees xtp  (*get the formal parameter list*)
+            val Ts = map type_of args0
+            val extraTs = rhs_extra_types (Ts ---> T) xtp
+            val _ = if null extraTs then () else
+              warning ("Skolemization: extra type vars: " ^
+                commas_quote (map (Syntax.string_of_typ_global thy) extraTs))
+            val argsx = map (fn T => Free (gensym "vsk", T)) extraTs
+            val args = argsx @ args0
+            val cT = extraTs ---> Ts ---> T
+            val rhs = list_abs_free (map dest_Free args, HOLogic.choice_const T $ xtp)
+                    (*Forms a lambda-abstraction over the formal parameters*)
+            val (c, thy') = Sign.declare_const [Markup.property_internal] (cname, cT, NoSyn) thy
+            val cdef = cname ^ "_def"
+            val thy'' = Theory.add_defs_i true false [(cdef, equals cT $ c $ rhs)] thy'
+              handle ERROR _ => raise Clausify_failure thy'
+            val ax = Thm.get_axiom_i thy'' (Sign.full_name thy'' cdef)
+          in dec_sko (subst_bound (list_comb (c, args), p)) (ax :: axs, thy'') end
+      | dec_sko (Const ("All", _) $ (xtp as Abs (a, T, p))) thx =
+          (*Universal quant: insert a free variable into body and continue*)
+          let val fname = Name.variant (add_term_names (p, [])) a
+          in dec_sko (subst_bound (Free (fname, T), p)) thx end
+      | dec_sko (Const ("op &", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
+      | dec_sko (Const ("op |", _) $ p $ q) thx = dec_sko q (dec_sko p thx)
+      | dec_sko (Const ("Trueprop", _) $ p) thx = dec_sko p thx
+      | dec_sko t thx = thx (*Do nothing otherwise*)
+  in fn thy => dec_sko (Thm.prop_of th) ([], thy) end;
 
 (*Traverse a theorem, accumulating Skolem function definitions.*)
 fun assume_skofuns s th =
@@ -288,7 +286,7 @@
 
 
 (*This will refer to the final version of theory ATP_Linkup.*)
-val atp_linkup_thy_ref = Theory.check_thy @{theory}
+val atp_linkup_thy_ref = @{theory_ref}
 
 (*Transfer a theorem into theory ATP_Linkup.thy if it is not already
   inside that theory -- because it's needed for Skolemization.
@@ -371,7 +369,7 @@
 
 (*Declare Skolem functions for a theorem, supplied in nnf and with its name.
   It returns a modified theory, unless skolemization fails.*)
-fun skolem thy th =
+fun skolem th thy =
   let val ctxt0 = Variable.thm_context th
       val _ = Output.debug (fn () => "skolemizing " ^ name_or_string th)
   in
@@ -380,7 +378,7 @@
           let 
               val _ = Output.debug (fn () => "  initial nnf: " ^ Display.string_of_thm nnfth)
               val s = fake_name th
-              val (thy',defs) = declare_skofuns s nnfth thy
+              val (defs,thy') = declare_skofuns s nnfth thy
               val (cnfs,ctxt2) = Meson.make_cnf (map skolem_of_def defs) nnfth ctxt1
               val _ = Output.debug (fn () => Int.toString (length cnfs) ^ " clauses yielded")
               val cnfs' = cnfs |> map combinators |> Variable.export ctxt2 ctxt0 
@@ -407,7 +405,7 @@
 fun skolem_cache_thm th thy =
   case Thmtab.lookup (ThmCache.get thy) th of
       NONE =>
-        (case skolem thy (Thm.transfer thy th) of
+        (case skolem (Thm.transfer thy th) thy of
              NONE => ([th],thy)
            | SOME (cls,thy') =>
                  (Output.debug (fn () => "skolem_cache_thm: " ^ Int.toString (length cls) ^