# HG changeset patch
# User haftmann
# Date 1273044282 -7200
# Node ID d95f3944812114f0ef9877352348ee243b9a5607
# Parent  6d25e8dab1e393a9a2b9c7e95731ba5e59fa60cf
eq_morphism is always optional: avoid trivial morphism for empty list of equations

diff -r 6d25e8dab1e3 -r d95f39448121 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Wed May 05 09:24:41 2010 +0200
+++ b/src/Pure/Isar/class.ML	Wed May 05 09:24:42 2010 +0200
@@ -74,7 +74,10 @@
     fun prove_assm_intro thm =
       let
         val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
-        val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
+        val const_eq_morph = case eq_morph
+         of SOME eq_morph => const_morph $> eq_morph
+          | NONE => const_morph
+        val thm'' = Morphism.thm const_eq_morph thm';
         val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
       in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
     val assm_intro = Option.map prove_assm_intro
@@ -290,7 +293,9 @@
     |-> (fn (param_map, params, assm_axiom) =>
        `(fn thy => calculate thy class sups base_sort param_map assm_axiom)
     #-> (fn (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) =>
-       Locale.add_registration (class, base_morph $> eq_morph (*FIXME duplication*)) (SOME (eq_morph, true)) export_morph
+       Locale.add_registration (class, case eq_morph of SOME eq_morph => base_morph $> eq_morph | NONE => base_morph)
+         (*FIXME should avoid modification of base morphism, but then problem with sublocale linorder < distrib_lattice*)
+         (Option.map (rpair true) eq_morph) export_morph
     #> register class sups params base_sort base_morph export_morph axiom assm_intro of_class))
     |> Theory_Target.init (SOME class)
     |> pair class
diff -r 6d25e8dab1e3 -r d95f39448121 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Wed May 05 09:24:41 2010 +0200
+++ b/src/Pure/Isar/class_target.ML	Wed May 05 09:24:42 2010 +0200
@@ -151,8 +151,9 @@
 fun these_operations thy = maps (#operations o the_class_data thy) o ancestry thy;
 
 val base_morphism = #base_morph oo the_class_data;
-fun morphism thy class = base_morphism thy class
-  $> Element.eq_morphism thy (these_defs thy [class]);
+fun morphism thy class = case Element.eq_morphism thy (these_defs thy [class])
+ of SOME eq_morph => base_morphism thy class $> eq_morph
+  | NONE => base_morphism thy class;
 val export_morphism = #export_morph oo the_class_data;
 
 fun print_classes thy =
@@ -202,12 +203,11 @@
       #> fold (curry Graph.add_edge class) sups;
   in ClassData.map add_class thy end;
 
-fun activate_defs class thms thy =
-  let
-    val eq_morph = Element.eq_morphism thy thms;
-    fun amend cls thy = Locale.amend_registration (cls, base_morphism thy cls)
-      (eq_morph, true) (export_morphism thy cls) thy;
-  in fold amend (heritage thy [class]) thy end;
+fun activate_defs class thms thy = case Element.eq_morphism thy thms
+ of SOME eq_morph => fold (fn cls => fn thy =>
+      Locale.amend_registration (cls, base_morphism thy cls)
+        (eq_morph, true) (export_morphism thy cls) thy) (heritage thy [class]) thy
+  | NONE => thy;
 
 fun register_operation class (c, (t, some_def)) thy =
   let
@@ -223,7 +223,7 @@
       (fn (defs, operations) =>
         (fold cons (the_list some_def) defs,
           (c, (class, (ty', t'))) :: operations))
-    |> is_some some_def ? activate_defs class (the_list some_def)
+    |> activate_defs class (the_list some_def)
   end;
 
 fun register_subclass (sub, sup) some_dep_morph some_wit export thy =
diff -r 6d25e8dab1e3 -r d95f39448121 src/Pure/Isar/element.ML
--- a/src/Pure/Isar/element.ML	Wed May 05 09:24:41 2010 +0200
+++ b/src/Pure/Isar/element.ML	Wed May 05 09:24:42 2010 +0200
@@ -55,7 +55,7 @@
   val satisfy_facts: witness list ->
     (Attrib.binding * (thm list * Attrib.src list) list) list ->
     (Attrib.binding * (thm list * Attrib.src list) list) list
-  val eq_morphism: theory -> thm list -> morphism
+  val eq_morphism: theory -> thm list -> morphism option
   val transfer_morphism: theory -> morphism
   val init: context_i -> Context.generic -> Context.generic
   val activate_i: context_i -> Proof.context -> context_i * Proof.context
@@ -448,11 +448,11 @@
 
 (* rewriting with equalities *)
 
-fun eq_morphism thy thms = Morphism.morphism
+fun eq_morphism thy thms = if null thms then NONE else SOME (Morphism.morphism
  {binding = I,
   typ = I,
   term = MetaSimplifier.rewrite_term thy thms [],
-  fact = map (MetaSimplifier.rewrite_rule thms)};
+  fact = map (MetaSimplifier.rewrite_rule thms)});
 
 
 (* transfer to theory using closure *)
diff -r 6d25e8dab1e3 -r d95f39448121 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Wed May 05 09:24:41 2010 +0200
+++ b/src/Pure/Isar/expression.ML	Wed May 05 09:24:42 2010 +0200
@@ -821,7 +821,7 @@
       #-> (fn eqns => fold (fn ((dep, morph), wits) =>
         fn thy => Locale.add_registration (dep, morph $> Element.satisfy_morphism
             (map (Element.morph_witness export') wits))
-          (if null eqns then NONE else SOME (Element.eq_morphism thy eqns, true))
+          (Element.eq_morphism thy eqns |> Option.map (rpair true))
           export thy) (deps ~~ witss)));
 
   in Element.witness_proof_eqs after_qed propss eqns goal_ctxt end;