src/Pure/Isar/named_target.ML
changeset 40782 aa533c5e3f48
parent 39639 3dd559ab878b
child 41585 45d7da4e4ccf
     1.1 --- a/src/Pure/Isar/named_target.ML	Sun Nov 28 14:01:20 2010 +0100
     1.2 +++ b/src/Pure/Isar/named_target.ML	Sun Nov 28 15:28:48 2010 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4  
     1.5  (* generic declarations *)
     1.6  
     1.7 -fun locale_declaration locale { syntax, pervasive } decl lthy =
     1.8 +fun locale_declaration locale {syntax, pervasive} decl lthy =
     1.9    let
    1.10      val add = if syntax then Locale.add_syntax_declaration else Locale.add_declaration;
    1.11      val locale_decl = Morphism.transform (Local_Theory.target_morphism lthy) decl;
    1.12 @@ -48,9 +48,9 @@
    1.13      |> Local_Theory.target (add locale locale_decl)
    1.14    end;
    1.15  
    1.16 -fun target_declaration (Target {target, ...}) { syntax, pervasive } =
    1.17 +fun target_declaration (Target {target, ...}) {syntax, pervasive} =
    1.18    if target = "" then Generic_Target.theory_declaration
    1.19 -  else locale_declaration target { syntax = syntax, pervasive = pervasive };
    1.20 +  else locale_declaration target {syntax = syntax, pervasive = pervasive};
    1.21  
    1.22  
    1.23  (* consts in locales *)
    1.24 @@ -81,7 +81,7 @@
    1.25    end;
    1.26  
    1.27  fun locale_const_declaration (ta as Target {target, ...}) prmode arg =
    1.28 -  locale_declaration target { syntax = true, pervasive = false } (locale_const ta prmode arg);
    1.29 +  locale_declaration target {syntax = true, pervasive = false} (locale_const ta prmode arg);
    1.30  
    1.31  
    1.32  (* define *)
    1.33 @@ -106,7 +106,7 @@
    1.34  
    1.35  (* notes *)
    1.36  
    1.37 -fun locale_notes locale kind global_facts local_facts lthy = 
    1.38 +fun locale_notes locale kind global_facts local_facts lthy =
    1.39    let
    1.40      val global_facts' = Attrib.map_facts (K I) global_facts;
    1.41      val local_facts' = Element.facts_map
    1.42 @@ -119,7 +119,7 @@
    1.43  
    1.44  fun target_notes (Target {target, is_locale, ...}) =
    1.45    if is_locale then locale_notes target
    1.46 -    else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
    1.47 +  else fn kind => fn global_facts => fn _ => Generic_Target.theory_notes kind global_facts;
    1.48  
    1.49  
    1.50  (* abbrev *)
    1.51 @@ -156,10 +156,11 @@
    1.52      val elems =
    1.53        (if null fixes then [] else [Element.Fixes fixes]) @
    1.54        (if null assumes then [] else [Element.Assumes assumes]);
    1.55 -    val body_elems =  if not is_locale then []
    1.56 +    val body_elems =
    1.57 +      if not is_locale then []
    1.58        else if null elems then [Pretty.block target_name]
    1.59        else [Pretty.block (Pretty.fbreaks (Pretty.block (target_name @ [Pretty.str " ="]) ::
    1.60 -        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))]
    1.61 +        map (Pretty.chunks o Element.pretty_ctxt ctxt) elems))];
    1.62    in
    1.63      Pretty.block [Pretty.command "theory", Pretty.brk 1,
    1.64        Pretty.str (Context.theory_name (ProofContext.theory_of ctxt))] :: body_elems
    1.65 @@ -185,9 +186,9 @@
    1.66          notes = Generic_Target.notes (target_notes ta),
    1.67          abbrev = Generic_Target.abbrev (target_abbrev ta),
    1.68          declaration = fn pervasive => target_declaration ta
    1.69 -          { syntax = false, pervasive = pervasive },
    1.70 +          {syntax = false, pervasive = pervasive},
    1.71          syntax_declaration = fn pervasive => target_declaration ta
    1.72 -          { syntax = true, pervasive = pervasive },
    1.73 +          {syntax = true, pervasive = pervasive},
    1.74          pretty = pretty ta,
    1.75          exit = Local_Theory.target_of}
    1.76    end;