1.1 --- a/src/Pure/Isar/class_target.ML	Tue Jun 01 11:01:16 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Tue Jun 01 11:04:49 2010 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4        | NONE => I
     1.5    in
     1.6      thy
     1.7 -    |> AxClass.add_classrel classrel
     1.8 +    |> AxClass.add_classrel true 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 results);
    1.17 +      ProofContext.theory ((fold o fold) (AxClass.add_classrel true) results);
    1.18    in
    1.19      thy
    1.20      |> ProofContext.init_global
    1.21 @@ -531,7 +531,7 @@
    1.22      val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    1.23      val arities_proof = maps (fn tyco => Logic.mk_arities (tyco, map snd vs, sort)) tycos;
    1.24      fun after_qed' results =
    1.25 -      Local_Theory.theory (fold (AxClass.add_arity o Thm.varifyT_global) results)
    1.26 +      Local_Theory.theory (fold (AxClass.add_arity true o Thm.varifyT_global) results)
    1.27        #> after_qed;
    1.28    in
    1.29      lthy
    1.30 @@ -591,7 +591,7 @@
    1.31      val sorts = map snd vs;
    1.32      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
    1.33      fun after_qed results = ProofContext.theory
    1.34 -      ((fold o fold) AxClass.add_arity results);
    1.35 +      ((fold o fold) (AxClass.add_arity true) results);
    1.36    in
    1.37      thy
    1.38      |> ProofContext.init_global

     2.1 --- a/src/Pure/axclass.ML	Tue Jun 01 11:01:16 2010 +0200
     2.2 +++ b/src/Pure/axclass.ML	Tue Jun 01 11:04:49 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: thm -> theory -> theory
     2.8 -  val add_arity: thm -> theory -> theory
     2.9 +  val add_classrel: bool -> thm -> theory -> theory
    2.10 +  val add_arity: bool -> 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,46 +412,55 @@
    2.15  
    2.16  (* primitive rules *)
    2.17  
    2.18 -fun add_classrel raw_th thy =
    2.19 +fun 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      fun err () = raise THM ("add_classrel: malformed class relation", 0, [th]);
    2.24      val rel = Logic.dest_classrel prop handle TERM _ => err ();
    2.25      val (c1, c2) = cert_classrel thy rel handle TYPE _ => err ();
    2.26 -    val th' = th
    2.27 +    val (th', thy') =
    2.28 +      if store then PureThy.store_thm
    2.29 +        (Binding.name (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th) thy
    2.30 +      else (th, thy);
    2.31 +    val th'' = th'
    2.32        |> Thm.unconstrainT
    2.33 -      |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [])))] [];
    2.34 +      |> Drule.instantiate' [SOME (ctyp_of thy' (TVar ((Name.aT, 0), [])))] [];
    2.35    in
    2.36 -    thy
    2.37 +    thy'
    2.38      |> Sign.primitive_classrel (c1, c2)
    2.39 -    |> (#2 oo put_trancl_classrel) ((c1, c2), th')
    2.40 +    |> (#2 oo put_trancl_classrel) ((c1, c2), th'')
    2.41      |> perhaps complete_arities
    2.42    end;
    2.43  
    2.44 -fun add_arity raw_th thy =
    2.45 +fun add_arity store raw_th thy =
    2.46    let
    2.47      val th = Thm.strip_shyps (Thm.transfer thy raw_th);
    2.48      val prop = Thm.plain_prop_of th;
    2.49      fun err () = raise THM ("add_arity: malformed type arity", 0, [th]);
    2.50 -    val (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
    2.51 +    val arity as (t, Ss, c) = Logic.dest_arity prop handle TERM _ => err ();
    2.52 +
    2.53 +    val (th', thy') =
    2.54 +      if store then PureThy.store_thm
    2.55 +        (Binding.name (prefix arity_prefix (Logic.name_arity arity)), th) thy
    2.56 +      else (th, thy);
    2.57  
    2.58      val args = Name.names Name.context Name.aT Ss;
    2.59      val T = Type (t, map TFree args);
    2.60 -    val std_vars = map (fn (a, S) => SOME (ctyp_of thy (TVar ((a, 0), [])))) args;
    2.61 +    val std_vars = map (fn (a, S) => SOME (ctyp_of thy' (TVar ((a, 0), [])))) args;
    2.62  
    2.63 -    val missing_params = Sign.complete_sort thy [c]
    2.64 -      |> maps (these o Option.map #params o try (get_info thy))
    2.65 -      |> filter_out (fn (const, _) => can (get_inst_param thy) (const, t))
    2.66 +    val missing_params = Sign.complete_sort thy' [c]
    2.67 +      |> maps (these o Option.map #params o try (get_info thy'))
    2.68 +      |> filter_out (fn (const, _) => can (get_inst_param thy') (const, t))
    2.69        |> (map o apsnd o map_atyps) (K T);
    2.70 -    val th' = th
    2.71 +    val th'' = th'
    2.72        |> Thm.unconstrainT
    2.73        |> Drule.instantiate' std_vars [];
    2.74    in
    2.75 -    thy
    2.76 +    thy'
    2.77      |> fold (#2 oo declare_overloaded) missing_params
    2.78      |> Sign.primitive_arity (t, Ss, [c])
    2.79 -    |> put_arity ((t, Ss, c), th')
    2.80 +    |> put_arity ((t, Ss, c), th'')
    2.81    end;
    2.82  
    2.83  
    2.84 @@ -468,7 +477,7 @@
    2.85      thy
    2.86      |> PureThy.add_thms [((Binding.name
    2.87          (prefix classrel_prefix (Logic.name_classrel (c1, c2))), th), [])]
    2.88 -    |-> (fn [th'] => add_classrel th')
    2.89 +    |-> (fn [th'] => add_classrel false th')
    2.90    end;
    2.91  
    2.92  fun prove_arity raw_arity tac thy =
    2.93 @@ -484,7 +493,7 @@
    2.94    in
    2.95      thy
    2.96      |> PureThy.add_thms (map (rpair []) (map Binding.name names ~~ ths))
    2.97 -    |-> fold add_arity
    2.98 +    |-> fold (add_arity false)
    2.99    end;
   2.100  
   2.101  
   2.102 @@ -618,11 +627,11 @@
   2.103  
   2.104  fun ax_classrel prep =
   2.105    axiomatize (map o prep) (map Logic.mk_classrel)
   2.106 -    (map (prefix classrel_prefix o Logic.name_classrel)) add_classrel;
   2.107 +    (map (prefix classrel_prefix o Logic.name_classrel)) (add_classrel false);
   2.108  
   2.109  fun ax_arity prep =
   2.110    axiomatize (prep o ProofContext.init_global) Logic.mk_arities
   2.111 -    (map (prefix arity_prefix) o Logic.name_arities) add_arity;
   2.112 +    (map (prefix arity_prefix) o Logic.name_arities) (add_arity false);
   2.113  
   2.114  fun class_const c =
   2.115    (Logic.const_of_class c, Term.itselfT (Term.aT []) --> propT);