src/Pure/axclass.ML
changeset 37246 b3ff14122645
parent 37232 c10fb22a5e0c
child 37249 8365cbc31349
     1.1 --- a/src/Pure/axclass.ML	Tue Jun 01 13:59:13 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Jun 01 15:59:01 2010 +0200
     1.3 @@ -24,8 +24,8 @@
     1.4    val read_classrel: theory -> xstring * xstring -> class * class
     1.5    val declare_overloaded: string * typ -> theory -> term * theory
     1.6    val define_overloaded: binding -> string * term -> theory -> thm * theory
     1.7 -  val add_classrel: bool -> thm -> theory -> theory
     1.8 -  val add_arity: bool -> thm -> theory -> theory
     1.9 +  val add_classrel: thm -> theory -> theory
    1.10 +  val add_arity: thm -> theory -> theory
    1.11    val prove_classrel: class * class -> tactic -> theory -> theory
    1.12    val prove_arity: string * sort list * sort -> tactic -> theory -> theory
    1.13    val define_class: binding * class list -> string list ->
    1.14 @@ -412,7 +412,7 @@
    1.15  
    1.16  (* primitive rules *)
    1.17  
    1.18 -fun add_classrel store raw_th thy =
    1.19 +fun gen_add_classrel store raw_th thy =
    1.20    let
    1.21      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    1.22      val prop = Thm.plain_prop_of th;
    1.23 @@ -433,7 +433,7 @@
    1.24      |> perhaps complete_arities
    1.25    end;
    1.26  
    1.27 -fun add_arity store raw_th thy =
    1.28 +fun gen_add_arity store raw_th thy =
    1.29    let
    1.30      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    1.31      val prop = Thm.plain_prop_of th;
    1.32 @@ -463,6 +463,9 @@
    1.33      |> put_arity ((t, Ss, c), th'')
    1.34    end;
    1.35  
    1.36 +val add_classrel = gen_add_classrel true;
    1.37 +val add_arity = gen_add_arity true;
    1.38 +
    1.39  
    1.40  (* tactical proofs *)
    1.41  
    1.42 @@ -477,7 +480,7 @@
    1.43      thy
    1.44      |> PureThy.add_thms [((Binding.name
    1.45          (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
    1.46 -    |-> (fn [th'] => add_classrel false th')
    1.47 +    |-> (fn [th'] => gen_add_classrel false th')
    1.48    end;
    1.49  
    1.50  fun prove_arity raw_arity tac thy =
    1.51 @@ -493,7 +496,7 @@
    1.52    in
    1.53      thy
    1.54      |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
    1.55 -    |-> fold (add_arity false)
    1.56 +    |-> fold (gen_add_arity false)
    1.57    end;
    1.58  
    1.59  
    1.60 @@ -627,11 +630,11 @@
    1.61  
    1.62  fun ax_classrel prep =
    1.63    axiomatize (map o prep) (map Logic.mk_classrel)
    1.64 -    (map (prefix classrel_prefix o Logic.name_classrel)) (add_classrel false);
    1.65 +    (map (prefix classrel_prefix o Logic.name_classrel)) (gen_add_classrel false);
    1.66  
    1.67  fun ax_arity prep =
    1.68    axiomatize (prep o ProofContext.init_global) Logic.mk_arities
    1.69 -    (map (prefix arity_prefix) o Logic.name_arities) (add_arity false);
    1.70 +    (map (prefix arity_prefix) o Logic.name_arities) (gen_add_arity false);
    1.71  
    1.72  fun class_const c =
    1.73    (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);