src/HOL/Tools/res_axioms.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18833 bead1a4e966b
     1.1 --- a/src/HOL/Tools/res_axioms.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/res_axioms.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -484,18 +484,15 @@
     1.4  (*Conjoin a list of clauses to recreate a single theorem*)
     1.5  val conj_rule = foldr1 conj2_rule;
     1.6  
     1.7 -fun skolem_global_fun (thy, th) = 
     1.8 -  let val name = Thm.name_of_thm th
     1.9 -      val (cls,thy') = skolem_cache_thm ((name,th), thy)
    1.10 -  in  (thy', conj_rule cls)  end;
    1.11 -
    1.12 -val skolem_global = Attrib.no_args skolem_global_fun;
    1.13 -
    1.14 -fun skolem_local x = Attrib.no_args (Attrib.rule (K (conj_rule o skolem_thm))) x;
    1.15 +fun skolem (Context.Theory thy, th) =
    1.16 +      let
    1.17 +        val name = Thm.name_of_thm th
    1.18 +        val (cls, thy') = skolem_cache_thm ((name, th), thy)
    1.19 +      in (Context.Theory thy', conj_rule cls) end
    1.20 +  | skolem (context, th) = (context, conj_rule (skolem_thm th));
    1.21  
    1.22  val setup_attrs = Attrib.add_attributes
    1.23 - [("skolem", (skolem_global, skolem_local),
    1.24 -    "skolemization of a theorem")];
    1.25 +  [("skolem", Attrib.no_args skolem, "skolemization of a theorem")];
    1.26  
    1.27  val setup = clause_cache_setup #> setup_attrs;
    1.28