# HG changeset patch
# User wenzelm
# Date 1320526879 -3600
# Node ID 0b4038361a3a68872e40cd3df2159fe7b3ecbfb5
# Parent  8b1604119bc0f22fd681229e5b16ea368b5a0c21
misc tuning;

diff -r 8b1604119bc0 -r 0b4038361a3a src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sat Nov 05 21:36:56 2011 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sat Nov 05 22:01:19 2011 +0100
@@ -106,14 +106,16 @@
     (*export assumes/defines*)
     val th = Goal.norm_result raw_th;
     val (defs, th') = Local_Defs.export ctxt thy_ctxt th;
-    val assms = map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
-      (Assumption.all_assms_of ctxt);
+    val assms =
+      map (Raw_Simplifier.rewrite_rule defs o Thm.assume)
+        (Assumption.all_assms_of ctxt);
     val nprems = Thm.nprems_of th' - Thm.nprems_of th;
 
     (*export fixes*)
     val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
     val frees = map Free (Thm.fold_terms Term.add_frees th' []);
-    val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
+    val (th'' :: vs) =
+      (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
       |> Variable.export ctxt thy_ctxt
       |> Drule.zero_var_indexes_list;
 
@@ -183,6 +185,7 @@
   end;
 
 
+
 (** primitive theory operations **)
 
 fun theory_declaration decl lthy =
diff -r 8b1604119bc0 -r 0b4038361a3a src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sat Nov 05 21:36:56 2011 +0100
+++ b/src/Pure/Isar/named_target.ML	Sat Nov 05 22:01:19 2011 +0100
@@ -65,46 +65,45 @@
 
 (* consts in locales *)
 
-fun locale_const (Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) phi =
-  let
-    val b' = Morphism.binding phi b;
-    val rhs' = Morphism.term phi rhs;
-    val arg = (b', Term.close_schematic_term rhs');
-    val same_shape = Term.aconv_untyped (rhs, rhs');
-    (* FIXME workaround based on educated guess *)
-    val prefix' = Binding.prefix_of b';
-    val is_canonical_class = is_class andalso
-      (Binding.eq_name (b, b')
-        andalso not (null prefix')
-        andalso List.last prefix' = (Class.class_prefix target, false)
-      orelse same_shape);
-  in
-    not is_canonical_class ?
-      (Context.mapping_result
-        (Sign.add_abbrev Print_Mode.internal arg)
-        (Proof_Context.add_abbrev Print_Mode.internal arg)
-      #-> (fn (lhs' as Const (d, _), _) =>
-          same_shape ?
-            (Context.mapping
-              (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
-             Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
-  end;
+fun locale_const (ta as Target {target, is_class, ...}) (prmode as (mode, _)) ((b, mx), rhs) =
+  locale_declaration target true (fn phi =>
+    let
+      val b' = Morphism.binding phi b;
+      val rhs' = Morphism.term phi rhs;
+      val arg = (b', Term.close_schematic_term rhs');
+      val same_shape = Term.aconv_untyped (rhs, rhs');
 
-fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
-  locale_declaration target true (locale_const ta prmode arg);
+      (* FIXME workaround based on educated guess *)
+      val prefix' = Binding.prefix_of b';
+      val is_canonical_class = is_class andalso
+        (Binding.eq_name (b, b')
+          andalso not (null prefix')
+          andalso List.last prefix' = (Class.class_prefix target, false)
+        orelse same_shape);
+    in
+      not is_canonical_class ?
+        (Context.mapping_result
+          (Sign.add_abbrev Print_Mode.internal arg)
+          (Proof_Context.add_abbrev Print_Mode.internal arg)
+        #-> (fn (lhs' as Const (d, _), _) =>
+            same_shape ?
+              (Context.mapping
+                (Sign.revert_abbrev mode d) (Proof_Context.revert_abbrev mode d) #>
+               Morphism.form (Proof_Context.target_notation true prmode [(lhs', mx)]))))
+    end);
 
 
 (* define *)
 
 fun locale_foundation ta (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
-  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, mx), lhs)
+  #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, mx), lhs)
     #> pair (lhs, def))
 
 fun class_foundation (ta as Target {target, ...})
     (((b, U), mx), (b_def, rhs)) (type_params, term_params) =
   Generic_Target.theory_foundation (((b, U), NoSyn), (b_def, rhs)) (type_params, term_params)
-  #-> (fn (lhs, def) => locale_const_declaration ta Syntax.mode_default ((b, NoSyn), lhs)
+  #-> (fn (lhs, def) => locale_const ta Syntax.mode_default ((b, NoSyn), lhs)
     #> Class.const target ((b, mx), (type_params, lhs))
     #> pair (lhs, def))
 
@@ -137,7 +136,7 @@
 fun locale_abbrev ta prmode ((b, mx), t) xs =
   Local_Theory.background_theory_result
     (Sign.add_abbrev Print_Mode.internal (b, t)) #->
-      (fn (lhs, _) => locale_const_declaration ta prmode
+      (fn (lhs, _) => locale_const ta prmode
         ((b, mx), Term.list_comb (Logic.unvarify_global lhs, xs)));
 
 fun target_abbrev (ta as Target {target, is_locale, is_class, ...})
@@ -204,7 +203,8 @@
 
 fun reinit lthy =
   (case Data.get lthy of
-    SOME (Target {target, before_exit, ...}) => init before_exit target o Local_Theory.exit_global
+    SOME (Target {target, before_exit, ...}) =>
+      init before_exit target o Local_Theory.exit_global
   | NONE => error "Not in a named target");
 
 fun context_cmd "-" thy = init I "" thy