1.1 --- a/src/Pure/Isar/class_target.ML	Tue Jun 01 13:59:13 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Tue Jun 01 15:59:01 2010 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4        | NONE => I
     1.5    in
     1.6      thy
     1.7 -    |> AxClass.add_classrel true classrel
     1.8 +    |> AxClass.add_classrel classrel
     1.9      |> ClassData.map (Graph.add_edge (sub, sup))
    1.10      |> activate_defs sub (these_defs thy diff_sort)
    1.11      |> add_dependency
    1.12 @@ -366,7 +366,7 @@
    1.13  fun gen_classrel mk_prop classrel thy =
    1.14    let
    1.15      fun after_qed results =
    1.16 -      ProofContext.theory ((fold o fold) (AxClass.add_classrel true) results);
    1.17 +      ProofContext.theory ((fold o fold) AxClass.add_classrel results);
    1.18    in
    1.19      thy
    1.20      |> ProofContext.init_global
    1.21 @@ -450,7 +450,7 @@
    1.22  
    1.23  (* target *)
    1.24  
    1.25 -val sanatize_name = (*FIXME*)
    1.26 +val sanitize_name = (*FIXME*)
    1.27    let
    1.28      fun is_valid s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
    1.29        orelse s = "'" orelse s = "_";
    1.30 @@ -467,7 +467,7 @@
    1.31  
    1.32  fun type_name "*" = "prod"
    1.33    | type_name "+" = "sum"
    1.34 -  | type_name s = sanatize_name (Long_Name.base_name s);
    1.35 +  | type_name s = sanitize_name (Long_Name.base_name s);
    1.36  
    1.37  fun resort_terms pp algebra consts constraints ts =
    1.38    let
    1.39 @@ -531,7 +531,7 @@
    1.40      val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    1.41      val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
    1.42      fun after_qed' results =
    1.43 -      Local_Theory.theory (fold (AxClass.add_arity true o Thm.varifyT_global) results)
    1.44 +      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
    1.45        #> after_qed;
    1.46    in
    1.47      lthy
    1.48 @@ -591,7 +591,7 @@
    1.49      val sorts = map snd vs;
    1.50      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
    1.51      fun after_qed results = ProofContext.theory
    1.52 -      ((fold o fold) (AxClass.add_arity true) results);
    1.53 +      ((fold o fold) AxClass.add_arity results);
    1.54    in
    1.55      thy
    1.56      |> ProofContext.init_global

     2.1 --- a/src/Pure/axclass.ML	Tue Jun 01 13:59:13 2010 +0200
     2.2 +++ b/src/Pure/axclass.ML	Tue Jun 01 15:59:01 2010 +0200
     2.3 @@ -24,8 +24,8 @@
     2.4    val read_classrel: theory -> xstring * xstring -> class * class
     2.5    val declare_overloaded: string * typ -> theory -> term * theory
     2.6    val define_overloaded: binding -> string * term -> theory -> thm * theory
     2.7 -  val add_classrel: bool -> thm -> theory -> theory
     2.8 -  val add_arity: bool -> thm -> theory -> theory
     2.9 +  val add_classrel: thm -> theory -> theory
    2.10 +  val add_arity: thm -> theory -> theory
    2.11    val prove_classrel: class * class -> tactic -> theory -> theory
    2.12    val prove_arity: string * sort list * sort -> tactic -> theory -> theory
    2.13    val define_class: binding * class list -> string list ->
    2.14 @@ -412,7 +412,7 @@
    2.15  
    2.16  (* primitive rules *)
    2.17  
    2.18 -fun add_classrel store raw_th thy =
    2.19 +fun gen_add_classrel store raw_th thy =
    2.20    let
    2.21      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    2.22      val prop = Thm.plain_prop_of th;
    2.23 @@ -433,7 +433,7 @@
    2.24      |> perhaps complete_arities
    2.25    end;
    2.26  
    2.27 -fun add_arity store raw_th thy =
    2.28 +fun gen_add_arity store raw_th thy =
    2.29    let
    2.30      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    2.31      val prop = Thm.plain_prop_of th;
    2.32 @@ -463,6 +463,9 @@
    2.33      |> put_arity ((t, Ss, c), th'')
    2.34    end;
    2.35  
    2.36 +val add_classrel = gen_add_classrel true;
    2.37 +val add_arity = gen_add_arity true;
    2.38 +
    2.39  
    2.40  (* tactical proofs *)
    2.41  
    2.42 @@ -477,7 +480,7 @@
    2.43      thy
    2.44      |> PureThy.add_thms [((Binding.name
    2.45          (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
    2.46 -    |-> (fn [th'] => add_classrel false th')
    2.47 +    |-> (fn [th'] => gen_add_classrel false th')
    2.48    end;
    2.49  
    2.50  fun prove_arity raw_arity tac thy =
    2.51 @@ -493,7 +496,7 @@
    2.52    in
    2.53      thy
    2.54      |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
    2.55 -    |-> fold (add_arity false)
    2.56 +    |-> fold (gen_add_arity false)
    2.57    end;
    2.58  
    2.59  
    2.60 @@ -627,11 +630,11 @@
    2.61  
    2.62  fun ax_classrel prep =
    2.63    axiomatize (map o prep) (map Logic.mk_classrel)
    2.64 -    (map (prefix classrel_prefix o Logic.name_classrel)) (add_classrel false);
    2.65 +    (map (prefix classrel_prefix o Logic.name_classrel)) (gen_add_classrel false);
    2.66  
    2.67  fun ax_arity prep =
    2.68    axiomatize (prep o ProofContext.init_global) Logic.mk_arities
    2.69 -    (map (prefix arity_prefix) o Logic.name_arities) (add_arity false);
    2.70 +    (map (prefix arity_prefix) o Logic.name_arities) (gen_add_arity false);
    2.71  
    2.72  fun class_const c =
    2.73    (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);