# HG changeset patch
# User wenzelm
# Date 1290954528 -3600
# Node ID aa533c5e3f486cb138dda9f6b9753b8aa505ae43
# Parent  ba5be5c3d47741c114516154f78651b78189bcef
superficial tuning;

diff -r ba5be5c3d477 -r aa533c5e3f48 src/Pure/Isar/generic_target.ML
--- a/src/Pure/Isar/generic_target.ML	Sun Nov 28 14:01:20 2010 +0100
+++ b/src/Pure/Isar/generic_target.ML	Sun Nov 28 15:28:48 2010 +0100
@@ -7,28 +7,25 @@
 
 signature GENERIC_TARGET =
 sig
-  val define: (((binding * typ) * mixfix) * (binding * term)
-    -> term list * term list -> local_theory -> (term * thm) * local_theory)
-    -> (binding * mixfix) * (Attrib.binding * term) -> local_theory
-    -> (term * (string * thm)) * local_theory
-  val notes: (string
-    -> (Attrib.binding * (thm list * Args.src list) list) list
-    -> (Attrib.binding * (thm list * Args.src list) list) list
-    -> local_theory -> local_theory)
-    -> string -> (Attrib.binding * (thm list * Args.src list) list) list
-    -> local_theory -> (string * thm list) list * local_theory
-  val abbrev: (string * bool -> binding * mixfix -> term * term
-    -> term list -> local_theory -> local_theory)
-    -> string * bool -> (binding * mixfix) * term -> local_theory
-    -> (term * term) * local_theory
+  val define: (((binding * typ) * mixfix) * (binding * term) ->
+      term list * term list -> local_theory -> (term * thm) * local_theory) ->
+    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
+    (term * (string * thm)) * local_theory
+  val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+      (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
+    string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
+    (string * thm list) list * local_theory
+  val abbrev: (string * bool -> binding * mixfix -> term * term ->
+      term list -> local_theory -> local_theory) ->
+    string * bool -> (binding * mixfix) * term -> local_theory ->
+    (term * term) * local_theory
 
   val theory_declaration: declaration -> local_theory -> local_theory
-  val theory_foundation: ((binding * typ) * mixfix) * (binding * term)
-    -> term list * term list -> local_theory -> (term * thm) * local_theory
-  val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list
-    -> local_theory -> local_theory
-  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term
-    -> local_theory -> local_theory
+  val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
+    term list * term list -> local_theory -> (term * thm) * local_theory
+  val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
+    local_theory -> local_theory
+  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
 end;
 
 structure Generic_Target: GENERIC_TARGET =
diff -r ba5be5c3d477 -r aa533c5e3f48 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Nov 28 14:01:20 2010 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Nov 28 15:28:48 2010 +0100
@@ -79,7 +79,7 @@
   val print_locale: theory -> bool -> xstring -> unit
   val print_registrations: Proof.context -> string -> unit
   val locale_deps: theory ->
-    { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
+    {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
       * term list list Symtab.table Symtab.table
 end;
 
@@ -191,10 +191,9 @@
     val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
     val ts = instance_of thy name morph;
   in
-    case qs of
-       [] => prt_inst ts
-     | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
-         Pretty.brk 1, prt_inst ts]
+    (case qs of
+      [] => prt_inst ts
+    | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts])
   end;
 
 
@@ -206,9 +205,9 @@
 
 (* total order *)
 fun ident_ord ((n: string, ts), (m, ss)) =
-  case fast_string_ord (m, n) of
-      EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
-    | ord => ord;
+  (case fast_string_ord (m, n) of
+    EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
+  | ord => ord);
 
 local
 
@@ -256,7 +255,8 @@
       then (deps, marked)
       else
         let
-          val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
+          val dependencies' =
+            map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
           val marked' = (name, instance) :: marked;
           val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
         in
@@ -309,9 +309,10 @@
         val (_, s1) = Idtab.lookup reg1 id |> the;
         val (morph2, s2) = Idtab.lookup reg2 id |> the;
         val reg2' = Idtab.update (id, (morph2, s1)) reg2;
-        val mix2' = case Inttab.lookup mix2 s2 of
-              NONE => mix2 |
-              SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs);
+        val mix2' =
+          (case Inttab.lookup mix2 s2 of
+            NONE => mix2
+          | SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs));
         val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
         (* FIXME print interpretations,
            which is not straightforward without theory context *)
@@ -335,9 +336,9 @@
     val thy = Context.theory_of context;
     val (regs, mixins) = Registrations.get context;
   in
-    case Idtab.lookup regs (name, instance_of thy name morph) of
+    (case Idtab.lookup regs (name, instance_of thy name morph) of
       NONE => []
-    | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial)
+    | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial))
   end;
 
 fun compose_mixins mixins =
@@ -385,9 +386,12 @@
     val {notes, ...} = the_locale thy name;
     fun activate ((kind, facts), _) input =
       let
-        val mixin = case export' of NONE => Morphism.identity
-         | SOME export => collect_mixins context (name, morph $> export) $> export;
-        val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin))
+        val mixin =
+          (case export' of
+            NONE => Morphism.identity
+          | SOME export => collect_mixins context (name, morph $> export) $> export);
+        val facts' = facts
+          |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
       in activ_elem (Notes (kind, facts')) input end;
   in
     fold_rev activate notes input
@@ -401,9 +405,8 @@
         activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
       (* FIXME type parameters *)
       (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
-      (if not (null defs)
-        then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
-        else I);
+      (not (null defs) ?
+        activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)));
     val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
   in
     roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
@@ -443,12 +446,13 @@
     val regs = Registrations.get context |> fst;
     val base = instance_of thy name (morph $> export);
   in
-    case Idtab.lookup regs (name, base) of
-        NONE => error ("No interpretation of locale " ^
+    (case Idtab.lookup regs (name, base) of
+      NONE =>
+        error ("No interpretation of locale " ^
           quote (extern thy name) ^ " and\nparameter instantiation " ^
           space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
           " available")
-      | SOME (_, serial') => add_mixin serial' mixin context
+    | SOME (_, serial') => add_mixin serial' mixin context)
   end;
 
 (* Note that a registration that would be subsumed by an existing one will not be
@@ -457,8 +461,7 @@
 fun add_registration (name, base_morph) mixin export context =
   let
     val thy = Context.theory_of context;
-    val mix = case mixin of NONE => Morphism.identity
-          | SOME (mix, _) => mix;
+    val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
     val morph = base_morph $> mix;
     val inst = instance_of thy name morph;
   in
@@ -470,8 +473,10 @@
       |> roundup thy (add_reg thy export) export (name, morph)
       |> snd
       (* add mixin *)
-      |> (case mixin of NONE => I
-           | SOME mixin => amend_registration (name, morph) mixin export)
+      |>
+        (case mixin of
+          NONE => I
+        | SOME mixin => amend_registration (name, morph) mixin export)
       (* activate import hierarchy as far as not already active *)
       |> activate_facts (SOME export) (name, morph)
   end;
@@ -551,7 +556,7 @@
   Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
 
 
-(* Tactic *)
+(* Tactics *)
 
 fun gen_intro_locales_tac intros_tac eager ctxt =
   intros_tac
@@ -593,11 +598,10 @@
   let
     val thy = ProofContext.theory_of ctxt;
   in
-    (case registrations_of  (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
-        [] => Pretty.str ("no interpretations")
-      | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
-    |> Pretty.writeln
-  end;
+    (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
+      [] => Pretty.str ("no interpretations")
+    | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
+  end |> Pretty.writeln;
 
 fun locale_deps thy =
   let
@@ -605,16 +609,17 @@
     fun add_locale_node name =
       let
         val params = params_of thy name;
-        val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
-        val registrations = map (instance_of thy name o snd)
-          (registrations_of (Context.Theory thy) name);
-      in 
-        Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
+        val axioms =
+          these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
+        val registrations =
+          map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
+      in
+        Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
       end;
     fun add_locale_deps name =
       let
-        val dependencies = (map o apsnd) (instance_of thy name o op $>)
-          (dependencies_of thy name);
+        val dependencies =
+          (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name);
       in
         fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
           deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))
diff -r ba5be5c3d477 -r aa533c5e3f48 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Sun Nov 28 14:01:20 2010 +0100
+++ b/src/Pure/Isar/named_target.ML	Sun Nov 28 15:28:48 2010 +0100
@@ -38,7 +38,7 @@
 
 (* generic declarations *)
 
-fun locale_declaration locale { syntax, pervasive } decl lthy =
+fun locale_declaration locale {syntax, pervasive} decl lthy =
   let
     val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
     val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
@@ -48,9 +48,9 @@
     |> Local_Theory.target (add locale locale_decl)
   end;
 
-fun target_declaration (Target {target, ...}) { syntax, pervasive } =
+fun target_declaration (Target {target, ...}) {syntax, pervasive} =
   if target = "" then Generic_Target.theory_declaration
-  else locale_declaration target { syntax = syntax, pervasive = pervasive };
+  else locale_declaration target {syntax = syntax, pervasive = pervasive};
 
 
 (* consts in locales *)
@@ -81,7 +81,7 @@
   end;
 
 fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
-  locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
+  locale_declaration target {syntax = true, pervasive = false} (locale_const ta prmode arg);
 
 
 (* define *)
@@ -106,7 +106,7 @@
 
 (* notes *)
 
-fun locale_notes locale kind global_facts local_facts lthy = 
+fun locale_notes locale kind global_facts local_facts lthy =
   let
     val global_facts' = Attrib.map_facts (K I) global_facts;
     val local_facts' = Element.facts_map
@@ -119,7 +119,7 @@
 
 fun target_notes (Target {target, is_locale, ...}) =
   if is_locale then locale_notes target
-    else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
+  else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
 
 
 (* abbrev *)
@@ -156,10 +156,11 @@
     val elems =
       (if null fixes then [] else [Element.Fixes fixes]) @
       (if null assumes then [] else [Element.Assumes assumes]);
-    val body_elems =  if not is_locale then []
+    val body_elems =
+      if not is_locale then []
       else if null elems then [Pretty.block target_name]
       else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
-        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
+        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
   in
     Pretty.block [Pretty.command "theory", Pretty.brk 1,
       Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems
@@ -185,9 +186,9 @@
         notes = Generic_Target.notes (target_notes ta),
         abbrev = Generic_Target.abbrev (target_abbrev ta),
         declaration = fn pervasive => target_declaration ta
-          { syntax = false, pervasive = pervasive },
+          {syntax = false, pervasive = pervasive},
         syntax_declaration = fn pervasive => target_declaration ta
-          { syntax = true, pervasive = pervasive },
+          {syntax = true, pervasive = pervasive},
         pretty = pretty ta,
         exit = Local_Theory.target_of}
   end;
diff -r ba5be5c3d477 -r aa533c5e3f48 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Nov 28 14:01:20 2010 +0100
+++ b/src/Pure/Isar/overloading.ML	Sun Nov 28 15:28:48 2010 +0100
@@ -48,15 +48,16 @@
 );
 
 fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints,
-  secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } => let
+    secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } =>
+  let
     val (((primary_constraints', secondary_constraints'),
       (((improve', subst'), consider_abbrevs'), unchecks')), passed')
         = f (((primary_constraints, secondary_constraints),
             (((improve, subst), consider_abbrevs), unchecks)), passed)
   in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
     improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
-    unchecks = unchecks', passed = passed'
-  } end);
+    unchecks = unchecks', passed = passed' }
+  end);
 
 val mark_passed = (map_improvable_syntax o apsnd) (K true);
 
@@ -80,7 +81,8 @@
           | NONE => NONE)
         | _ => NONE) t;
     val ts'' = if is_abbrev then ts' else map apply_subst ts';
-  in if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
+  in
+    if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
     if passed_or_abbrev then SOME (ts'', ctxt)
     else SOME (ts'', ctxt
       |> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints
@@ -166,9 +168,11 @@
 fun conclude lthy =
   let
     val overloading = get_overloading lthy;
-    val _ = if null overloading then () else
-      error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
-        o Syntax.string_of_term lthy o Const o fst) overloading));
+    val _ =
+      if null overloading then ()
+      else
+        error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
+          o Syntax.string_of_term lthy o Const o fst) overloading));
   in lthy end;
 
 fun gen_overloading prep_const raw_overloading thy =