1.1 --- a/src/Pure/axclass.ML	Tue Jun 01 22:19:17 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Wed Jun 02 08:01:45 2010 +0200
     1.3 @@ -412,17 +412,15 @@
     1.4  
     1.5  (* primitive rules *)
     1.6  
     1.7 -fun gen_add_classrel store raw_th thy =
     1.8 +fun add_classrel raw_th thy =
     1.9    let
    1.10      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    1.11      val prop = Thm.plain_prop_of th;
    1.12      fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
    1.13      val rel = Logic.dest_classrel prop handle TERM _ => err ();
    1.14      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    1.15 -    val (th', thy') =
    1.16 -      if store then PureThy.store_thm
    1.17 -        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy
    1.18 -      else (th, thy);
    1.19 +    val (th', thy') = PureThy.store_thm
    1.20 +      (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy;
    1.21      val th'' = th'
    1.22        |> Thm.unconstrainT
    1.23        |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
    1.24 @@ -433,17 +431,15 @@
    1.25      |> perhaps complete_arities
    1.26    end;
    1.27  
    1.28 -fun gen_add_arity store raw_th thy =
    1.29 +fun add_arity raw_th thy =
    1.30    let
    1.31      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    1.32      val prop = Thm.plain_prop_of th;
    1.33      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
    1.34      val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
    1.35  
    1.36 -    val (th', thy') =
    1.37 -      if store then PureThy.store_thm
    1.38 -        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy
    1.39 -      else (th, thy);
    1.40 +    val (th', thy') = PureThy.store_thm
    1.41 +      (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy;
    1.42  
    1.43      val args = Name.names Name.context Name.aT Ss;
    1.44      val T = Type (t, map TFree args);
    1.45 @@ -463,9 +459,6 @@
    1.46      |> put_arity ((t, Ss, c), th'')
    1.47    end;
    1.48  
    1.49 -val add_classrel = gen_add_classrel true;
    1.50 -val add_arity = gen_add_arity true;
    1.51 -
    1.52  
    1.53  (* tactical proofs *)
    1.54  
    1.55 @@ -477,10 +470,7 @@
    1.56        cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
    1.57          quote (Syntax.string_of_classrel ctxt [c1, c2]));
    1.58    in
    1.59 -    thy
    1.60 -    |> PureThy.add_thms [((Binding.name
    1.61 -        (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
    1.62 -    |-> (fn [th'] => gen_add_classrel false th')
    1.63 +    thy |> add_classrel th
    1.64    end;
    1.65  
    1.66  fun prove_arity raw_arity tac thy =
    1.67 @@ -494,9 +484,7 @@
    1.68          cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
    1.69            quote (Syntax.string_of_arity ctxt arity));
    1.70    in
    1.71 -    thy
    1.72 -    |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
    1.73 -    |-> fold (gen_add_arity false)
    1.74 +    thy |> fold add_arity ths
    1.75    end;
    1.76  
    1.77  
    1.78 @@ -613,10 +601,6 @@
    1.79  local
    1.80  
    1.81  (*old-style axioms*)
    1.82 -fun add_axiom (b, prop) =
    1.83 -  Thm.add_axiom (b, prop) #->
    1.84 -  (fn (_, thm) => PureThy.add_thm ((b, Drule.export_without_context thm), []));
    1.85 -
    1.86  fun axiomatize prep mk name add raw_args thy =
    1.87    let
    1.88      val args = prep thy raw_args;
    1.89 @@ -624,17 +608,17 @@
    1.90      val names = name args;
    1.91    in
    1.92      thy
    1.93 -    |> fold_map add_axiom (map Binding.name names ~~ specs)
    1.94 -    |-> fold add
    1.95 +    |> fold_map Thm.add_axiom (map Binding.name names ~~ specs)
    1.96 +    |-> fold (add o Drule.export_without_context o snd)
    1.97    end;
    1.98  
    1.99  fun ax_classrel prep =
   1.100    axiomatize (map o prep) (map Logic.mk_classrel)
   1.101 -    (map (prefix classrel_prefix o Logic.name_classrel)) (gen_add_classrel false);
   1.102 +    (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
   1.103  
   1.104  fun ax_arity prep =
   1.105    axiomatize (prep o ProofContext.init_global) Logic.mk_arities
   1.106 -    (map (prefix arity_prefix) o Logic.name_arities) (gen_add_arity false);
   1.107 +    (map (prefix arity_prefix) o Logic.name_arities) add_arity;
   1.108  
   1.109  fun class_const c =
   1.110    (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);