src/Pure/Isar/class.ML
changeset 29439 83601bdadae8
parent 29378 2821c2c5270d
child 29509 1ff0f3f08a7b
--- a/src/Pure/Isar/class.ML	Fri Jan 09 08:22:44 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sun Jan 11 14:18:16 2009 +0100
@@ -7,8 +7,8 @@
 signature CLASS =
 sig
   include CLASS_TARGET
-    (*FIXME the split in class_target.ML, theory_target.ML and
-      ML is artificial*)
+    (*FIXME the split into class_target.ML, theory_target.ML and
+      class.ML is artificial*)
 
   val class: bstring -> class list -> Element.context_i list
     -> theory -> string * local_theory
@@ -45,7 +45,25 @@
         |> SOME
       end;
 
-fun calculate_rules thy phi sups base_sort param_map axiom class =
+fun raw_morphism thy class param_map some_axiom =
+  let
+    val ctxt = ProofContext.init thy;
+    val some_wit = case some_axiom
+     of SOME axiom => SOME (Element.prove_witness ctxt
+          (Logic.unvarify (Thm.prop_of axiom))
+            (ALLGOALS (ProofContext.fact_tac [axiom])))
+      | NONE => NONE;
+    val instT = Symtab.empty |> Symtab.update ("'a", TFree ("'a", [class]));
+    val inst = Symtab.make ((map o apsnd) Const param_map);
+  in case some_wit
+   of SOME wit => Element.inst_morphism thy (instT, inst)
+        $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
+        $> Element.satisfy_morphism [wit]
+    | NONE => Element.inst_morphism thy (instT, inst)
+        $> Morphism.binding_morphism (Binding.add_prefix false (class_prefix class))
+  end;
+
+fun calculate_rules thy morph sups base_sort param_map axiom class =
   let
     fun instantiate thy sort = Thm.instantiate ([pairself (Thm.ctyp_of thy o TVar o pair (Name.aT, 0))
       (base_sort, sort)], map (fn (v, (c, ty)) => pairself (Thm.cterm_of thy)
@@ -200,14 +218,13 @@
     #-> (fn axiom =>
         prove_class_interpretation class inst
           (supconsts @ map (pair class o fst o snd) params) (the_list axiom) []
-    #-> (fn morphism =>
-        `(fn thy => activate_class_morphism thy class inst morphism)
-    #-> (fn phi =>
-        `(fn thy => calculate_rules thy phi sups base_sort param_map axiom class)
+    #> `(fn thy => raw_morphism thy class param_map axiom)
+    #-> (fn morph =>
+        `(fn thy => calculate_rules thy morph sups base_sort param_map axiom class)
     #-> (fn (assm_intro, of_class) =>
         register class sups params base_sort inst
-          morphism axiom assm_intro of_class
-    #> fold (note_assm_intro class) (the_list assm_intro))))))
+          morph axiom assm_intro of_class
+    #> fold (note_assm_intro class) (the_list assm_intro)))))
     |> TheoryTarget.init (SOME class)
     |> pair class
   end;