1.1 --- a/src/Pure/Isar/generic_target.ML	Sun Nov 28 14:01:20 2010 +0100
     1.2 +++ b/src/Pure/Isar/generic_target.ML	Sun Nov 28 15:28:48 2010 +0100
     1.3 @@ -7,28 +7,25 @@
     1.4  
     1.5  signature GENERIC_TARGET =
     1.6  sig
     1.7 -  val define: (((binding * typ) * mixfix) * (binding * term)
     1.8 -    -> term list * term list -> local_theory -> (term * thm) * local_theory)
     1.9 -    -> (binding * mixfix) * (Attrib.binding * term) -> local_theory
    1.10 -    -> (term * (string * thm)) * local_theory
    1.11 -  val notes: (string
    1.12 -    -> (Attrib.binding * (thm list * Args.src list) list) list
    1.13 -    -> (Attrib.binding * (thm list * Args.src list) list) list
    1.14 -    -> local_theory -> local_theory)
    1.15 -    -> string -> (Attrib.binding * (thm list * Args.src list) list) list
    1.16 -    -> local_theory -> (string * thm list) list * local_theory
    1.17 -  val abbrev: (string * bool -> binding * mixfix -> term * term
    1.18 -    -> term list -> local_theory -> local_theory)
    1.19 -    -> string * bool -> (binding * mixfix) * term -> local_theory
    1.20 -    -> (term * term) * local_theory
    1.21 +  val define: (((binding * typ) * mixfix) * (binding * term) ->
    1.22 +      term list * term list -> local_theory -> (term * thm) * local_theory) ->
    1.23 +    (binding * mixfix) * (Attrib.binding * term) -> local_theory ->
    1.24 +    (term * (string * thm)) * local_theory
    1.25 +  val notes: (string -> (Attrib.binding * (thm list * Args.src list) list) list ->
    1.26 +      (Attrib.binding * (thm list * Args.src list) list) list -> local_theory -> local_theory) ->
    1.27 +    string -> (Attrib.binding * (thm list * Args.src list) list) list -> local_theory ->
    1.28 +    (string * thm list) list * local_theory
    1.29 +  val abbrev: (string * bool -> binding * mixfix -> term * term ->
    1.30 +      term list -> local_theory -> local_theory) ->
    1.31 +    string * bool -> (binding * mixfix) * term -> local_theory ->
    1.32 +    (term * term) * local_theory
    1.33  
    1.34    val theory_declaration: declaration -> local_theory -> local_theory
    1.35 -  val theory_foundation: ((binding * typ) * mixfix) * (binding * term)
    1.36 -    -> term list * term list -> local_theory -> (term * thm) * local_theory
    1.37 -  val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list
    1.38 -    -> local_theory -> local_theory
    1.39 -  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term
    1.40 -    -> local_theory -> local_theory
    1.41 +  val theory_foundation: ((binding * typ) * mixfix) * (binding * term) ->
    1.42 +    term list * term list -> local_theory -> (term * thm) * local_theory
    1.43 +  val theory_notes: string -> (Attrib.binding * (thm list * Args.src list) list) list ->
    1.44 +    local_theory -> local_theory
    1.45 +  val theory_abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory -> local_theory
    1.46  end;
    1.47  
    1.48  structure Generic_Target: GENERIC_TARGET =

     2.1 --- a/src/Pure/Isar/locale.ML	Sun Nov 28 14:01:20 2010 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Sun Nov 28 15:28:48 2010 +0100
     2.3 @@ -79,7 +79,7 @@
     2.4    val print_locale: theory -> bool -> xstring -> unit
     2.5    val print_registrations: Proof.context -> string -> unit
     2.6    val locale_deps: theory ->
     2.7 -    { params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list } Graph.T
     2.8 +    {params: ((string * typ) * mixfix) list, axioms: term list, registrations: term list list} Graph.T
     2.9        * term list list Symtab.table Symtab.table
    2.10  end;
    2.11  
    2.12 @@ -191,10 +191,9 @@
    2.13      val qs = Binding.name "x" |> Morphism.binding morph |> Binding.prefix_of;
    2.14      val ts = instance_of thy name morph;
    2.15    in
    2.16 -    case qs of
    2.17 -       [] => prt_inst ts
    2.18 -     | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":",
    2.19 -         Pretty.brk 1, prt_inst ts]
    2.20 +    (case qs of
    2.21 +      [] => prt_inst ts
    2.22 +    | qs => Pretty.block [prt_quals qs, Pretty.brk 1, Pretty.str ":", Pretty.brk 1, prt_inst ts])
    2.23    end;
    2.24  
    2.25  
    2.26 @@ -206,9 +205,9 @@
    2.27  
    2.28  (* total order *)
    2.29  fun ident_ord ((n: string, ts), (m, ss)) =
    2.30 -  case fast_string_ord (m, n) of
    2.31 -      EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
    2.32 -    | ord => ord;
    2.33 +  (case fast_string_ord (m, n) of
    2.34 +    EQUAL => list_ord Term_Ord.fast_term_ord (ts, ss)
    2.35 +  | ord => ord);
    2.36  
    2.37  local
    2.38  
    2.39 @@ -256,7 +255,8 @@
    2.40        then (deps, marked)
    2.41        else
    2.42          let
    2.43 -          val dependencies' = map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
    2.44 +          val dependencies' =
    2.45 +            map (fn (name, (morph', export')) => (name, morph' $> export' $> morph)) dependencies;
    2.46            val marked' = (name, instance) :: marked;
    2.47            val (deps', marked'') = fold_rev (add thy (depth + 1) export) dependencies' ([], marked');
    2.48          in
    2.49 @@ -309,9 +309,10 @@
    2.50          val (_, s1) = Idtab.lookup reg1 id |> the;
    2.51          val (morph2, s2) = Idtab.lookup reg2 id |> the;
    2.52          val reg2' = Idtab.update (id, (morph2, s1)) reg2;
    2.53 -        val mix2' = case Inttab.lookup mix2 s2 of
    2.54 -              NONE => mix2 |
    2.55 -              SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs);
    2.56 +        val mix2' =
    2.57 +          (case Inttab.lookup mix2 s2 of
    2.58 +            NONE => mix2
    2.59 +          | SOME mxs => Inttab.delete s2 mix2 |> Inttab.update_new (s1, mxs));
    2.60          val _ = warning "Removed duplicate interpretation after retrieving its mixins.";
    2.61          (* FIXME print interpretations,
    2.62             which is not straightforward without theory context *)
    2.63 @@ -335,9 +336,9 @@
    2.64      val thy = Context.theory_of context;
    2.65      val (regs, mixins) = Registrations.get context;
    2.66    in
    2.67 -    case Idtab.lookup regs (name, instance_of thy name morph) of
    2.68 +    (case Idtab.lookup regs (name, instance_of thy name morph) of
    2.69        NONE => []
    2.70 -    | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial)
    2.71 +    | SOME (_, serial) => the_default [] (Inttab.lookup mixins serial))
    2.72    end;
    2.73  
    2.74  fun compose_mixins mixins =
    2.75 @@ -385,9 +386,12 @@
    2.76      val {notes, ...} = the_locale thy name;
    2.77      fun activate ((kind, facts), _) input =
    2.78        let
    2.79 -        val mixin = case export' of NONE => Morphism.identity
    2.80 -         | SOME export => collect_mixins context (name, morph $> export) $> export;
    2.81 -        val facts' = facts |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin))
    2.82 +        val mixin =
    2.83 +          (case export' of
    2.84 +            NONE => Morphism.identity
    2.85 +          | SOME export => collect_mixins context (name, morph $> export) $> export);
    2.86 +        val facts' = facts
    2.87 +          |> Element.facts_map (Element.morph_ctxt (transfer input $> morph $> mixin));
    2.88        in activ_elem (Notes (kind, facts')) input end;
    2.89    in
    2.90      fold_rev activate notes input
    2.91 @@ -401,9 +405,8 @@
    2.92          activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
    2.93        (* FIXME type parameters *)
    2.94        (case asm of SOME A => activ_elem (Assumes [(Attrib.empty_binding, [(A, [])])]) | _ => I) |>
    2.95 -      (if not (null defs)
    2.96 -        then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
    2.97 -        else I);
    2.98 +      (not (null defs) ?
    2.99 +        activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs)));
   2.100      val activate = activate_notes activ_elem transfer (Context.Theory thy) NONE;
   2.101    in
   2.102      roundup thy activate Morphism.identity (name, Morphism.identity) (marked, input')
   2.103 @@ -443,12 +446,13 @@
   2.104      val regs = Registrations.get context |> fst;
   2.105      val base = instance_of thy name (morph $> export);
   2.106    in
   2.107 -    case Idtab.lookup regs (name, base) of
   2.108 -        NONE => error ("No interpretation of locale " ^
   2.109 +    (case Idtab.lookup regs (name, base) of
   2.110 +      NONE =>
   2.111 +        error ("No interpretation of locale " ^
   2.112            quote (extern thy name) ^ " and\nparameter instantiation " ^
   2.113            space_implode " " (map (quote o Syntax.string_of_term_global thy) base) ^
   2.114            " available")
   2.115 -      | SOME (_, serial') => add_mixin serial' mixin context
   2.116 +    | SOME (_, serial') => add_mixin serial' mixin context)
   2.117    end;
   2.118  
   2.119  (* Note that a registration that would be subsumed by an existing one will not be
   2.120 @@ -457,8 +461,7 @@
   2.121  fun add_registration (name, base_morph) mixin export context =
   2.122    let
   2.123      val thy = Context.theory_of context;
   2.124 -    val mix = case mixin of NONE => Morphism.identity
   2.125 -          | SOME (mix, _) => mix;
   2.126 +    val mix = (case mixin of NONE => Morphism.identity | SOME (mix, _) => mix);
   2.127      val morph = base_morph $> mix;
   2.128      val inst = instance_of thy name morph;
   2.129    in
   2.130 @@ -470,8 +473,10 @@
   2.131        |> roundup thy (add_reg thy export) export (name, morph)
   2.132        |> snd
   2.133        (* add mixin *)
   2.134 -      |> (case mixin of NONE => I
   2.135 -           | SOME mixin => amend_registration (name, morph) mixin export)
   2.136 +      |>
   2.137 +        (case mixin of
   2.138 +          NONE => I
   2.139 +        | SOME mixin => amend_registration (name, morph) mixin export)
   2.140        (* activate import hierarchy as far as not already active *)
   2.141        |> activate_facts (SOME export) (name, morph)
   2.142    end;
   2.143 @@ -551,7 +556,7 @@
   2.144    Thm.declaration_attribute (fn th => Thms.map (fn (x, y, z) => (x, y, Thm.add_thm th z)));
   2.145  
   2.146  
   2.147 -(* Tactic *)
   2.148 +(* Tactics *)
   2.149  
   2.150  fun gen_intro_locales_tac intros_tac eager ctxt =
   2.151    intros_tac
   2.152 @@ -593,11 +598,10 @@
   2.153    let
   2.154      val thy = ProofContext.theory_of ctxt;
   2.155    in
   2.156 -    (case registrations_of  (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
   2.157 -        [] => Pretty.str ("no interpretations")
   2.158 -      | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
   2.159 -    |> Pretty.writeln
   2.160 -  end;
   2.161 +    (case registrations_of (Context.Proof ctxt) (* FIXME *) (intern thy raw_name) of
   2.162 +      [] => Pretty.str ("no interpretations")
   2.163 +    | regs => Pretty.big_list "interpretations:" (map (pretty_reg thy) (rev regs)))
   2.164 +  end |> Pretty.writeln;
   2.165  
   2.166  fun locale_deps thy =
   2.167    let
   2.168 @@ -605,16 +609,17 @@
   2.169      fun add_locale_node name =
   2.170        let
   2.171          val params = params_of thy name;
   2.172 -        val axioms = (these o Option.map (Logic.strip_imp_prems o Thm.prop_of) o fst o intros_of thy) name;
   2.173 -        val registrations = map (instance_of thy name o snd)
   2.174 -          (registrations_of (Context.Theory thy) name);
   2.175 -      in 
   2.176 -        Graph.new_node (name, { params = params, axioms = axioms, registrations = registrations })
   2.177 +        val axioms =
   2.178 +          these (Option.map (Logic.strip_imp_prems o Thm.prop_of) (fst (intros_of thy name)));
   2.179 +        val registrations =
   2.180 +          map (instance_of thy name o snd) (registrations_of (Context.Theory thy) name);
   2.181 +      in
   2.182 +        Graph.new_node (name, {params = params, axioms = axioms, registrations = registrations})
   2.183        end;
   2.184      fun add_locale_deps name =
   2.185        let
   2.186 -        val dependencies = (map o apsnd) (instance_of thy name o op $>)
   2.187 -          (dependencies_of thy name);
   2.188 +        val dependencies =
   2.189 +          (map o apsnd) (instance_of thy name o op $>) (dependencies_of thy name);
   2.190        in
   2.191          fold (fn (super, ts) => fn (gr, deps) => (gr |> Graph.add_edge (super, name),
   2.192            deps |> Symtab.map_default (super, Symtab.empty) (Symtab.cons_list (name, ts))))

     3.1 --- a/src/Pure/Isar/named_target.ML	Sun Nov 28 14:01:20 2010 +0100
     3.2 +++ b/src/Pure/Isar/named_target.ML	Sun Nov 28 15:28:48 2010 +0100
     3.3 @@ -38,7 +38,7 @@
     3.4  
     3.5  (* generic declarations *)
     3.6  
     3.7 -fun locale_declaration locale { syntax, pervasive } decl lthy =
     3.8 +fun locale_declaration locale {syntax, pervasive} decl lthy =
     3.9    let
    3.10      val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
    3.11      val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
    3.12 @@ -48,9 +48,9 @@
    3.13      |> Local_Theory.target (add locale locale_decl)
    3.14    end;
    3.15  
    3.16 -fun target_declaration (Target {target, ...}) { syntax, pervasive } =
    3.17 +fun target_declaration (Target {target, ...}) {syntax, pervasive} =
    3.18    if target = "" then Generic_Target.theory_declaration
    3.19 -  else locale_declaration target { syntax = syntax, pervasive = pervasive };
    3.20 +  else locale_declaration target {syntax = syntax, pervasive = pervasive};
    3.21  
    3.22  
    3.23  (* consts in locales *)
    3.24 @@ -81,7 +81,7 @@
    3.25    end;
    3.26  
    3.27  fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
    3.28 -  locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
    3.29 +  locale_declaration target {syntax = true, pervasive = false} (locale_const ta prmode arg);
    3.30  
    3.31  
    3.32  (* define *)
    3.33 @@ -106,7 +106,7 @@
    3.34  
    3.35  (* notes *)
    3.36  
    3.37 -fun locale_notes locale kind global_facts local_facts lthy = 
    3.38 +fun locale_notes locale kind global_facts local_facts lthy =
    3.39    let
    3.40      val global_facts' = Attrib.map_facts (K I) global_facts;
    3.41      val local_facts' = Element.facts_map
    3.42 @@ -119,7 +119,7 @@
    3.43  
    3.44  fun target_notes (Target {target, is_locale, ...}) =
    3.45    if is_locale then locale_notes target
    3.46 -    else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
    3.47 +  else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
    3.48  
    3.49  
    3.50  (* abbrev *)
    3.51 @@ -156,10 +156,11 @@
    3.52      val elems =
    3.53        (if null fixes then [] else [Element.Fixes fixes]) @
    3.54        (if null assumes then [] else [Element.Assumes assumes]);
    3.55 -    val body_elems =  if not is_locale then []
    3.56 +    val body_elems =
    3.57 +      if not is_locale then []
    3.58        else if null elems then [Pretty.block target_name]
    3.59        else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
    3.60 -        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
    3.61 +        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
    3.62    in
    3.63      Pretty.block [Pretty.command "theory", Pretty.brk 1,
    3.64        Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems
    3.65 @@ -185,9 +186,9 @@
    3.66          notes = Generic_Target.notes (target_notes ta),
    3.67          abbrev = Generic_Target.abbrev (target_abbrev ta),
    3.68          declaration = fn pervasive => target_declaration ta
    3.69 -          { syntax = false, pervasive = pervasive },
    3.70 +          {syntax = false, pervasive = pervasive},
    3.71          syntax_declaration = fn pervasive => target_declaration ta
    3.72 -          { syntax = true, pervasive = pervasive },
    3.73 +          {syntax = true, pervasive = pervasive},
    3.74          pretty = pretty ta,
    3.75          exit = Local_Theory.target_of}
    3.76    end;

     4.1 --- a/src/Pure/Isar/overloading.ML	Sun Nov 28 14:01:20 2010 +0100
     4.2 +++ b/src/Pure/Isar/overloading.ML	Sun Nov 28 15:28:48 2010 +0100
     4.3 @@ -48,15 +48,16 @@
     4.4  );
     4.5  
     4.6  fun map_improvable_syntax f = ImprovableSyntax.map (fn { primary_constraints,
     4.7 -  secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } => let
     4.8 +    secondary_constraints, improve, subst, consider_abbrevs, unchecks, passed } =>
     4.9 +  let
    4.10      val (((primary_constraints', secondary_constraints'),
    4.11        (((improve', subst'), consider_abbrevs'), unchecks')), passed')
    4.12          = f (((primary_constraints, secondary_constraints),
    4.13              (((improve, subst), consider_abbrevs), unchecks)), passed)
    4.14    in { primary_constraints = primary_constraints', secondary_constraints = secondary_constraints',
    4.15      improve = improve', subst = subst', consider_abbrevs = consider_abbrevs',
    4.16 -    unchecks = unchecks', passed = passed'
    4.17 -  } end);
    4.18 +    unchecks = unchecks', passed = passed' }
    4.19 +  end);
    4.20  
    4.21  val mark_passed = (map_improvable_syntax o apsnd) (K true);
    4.22  
    4.23 @@ -80,7 +81,8 @@
    4.24            | NONE => NONE)
    4.25          | _ => NONE) t;
    4.26      val ts'' = if is_abbrev then ts' else map apply_subst ts';
    4.27 -  in if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
    4.28 +  in
    4.29 +    if eq_list (op aconv) (ts, ts'') andalso passed_or_abbrev then NONE else
    4.30      if passed_or_abbrev then SOME (ts'', ctxt)
    4.31      else SOME (ts'', ctxt
    4.32        |> fold (ProofContext.add_const_constraint o apsnd SOME) secondary_constraints
    4.33 @@ -166,9 +168,11 @@
    4.34  fun conclude lthy =
    4.35    let
    4.36      val overloading = get_overloading lthy;
    4.37 -    val _ = if null overloading then () else
    4.38 -      error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
    4.39 -        o Syntax.string_of_term lthy o Const o fst) overloading));
    4.40 +    val _ =
    4.41 +      if null overloading then ()
    4.42 +      else
    4.43 +        error ("Missing definition(s) for parameter(s) " ^ commas (map (quote
    4.44 +          o Syntax.string_of_term lthy o Const o fst) overloading));
    4.45    in lthy end;
    4.46  
    4.47  fun gen_overloading prep_const raw_overloading thy =