src/Pure/Isar/theory_target.ML
changeset 29576 669b560fc2b9
parent 29393 172213e44992
child 29710 f2e70a0636b9
     1.1 --- a/src/Pure/Isar/theory_target.ML	Wed Jan 21 16:47:02 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Wed Jan 21 16:47:03 2009 +0100
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature THEORY_TARGET =
     1.6  sig
     1.7 -  val peek: local_theory -> {target: string, new_locale: bool, is_locale: bool,
     1.8 +  val peek: local_theory -> {target: string, is_locale: bool,
     1.9      is_class: bool, instantiation: string list * (string * sort) list * sort,
    1.10      overloading: (string * (string * typ) * bool) list}
    1.11    val init: string option -> theory -> local_theory
    1.12 @@ -21,34 +21,17 @@
    1.13  structure TheoryTarget: THEORY_TARGET =
    1.14  struct
    1.15  
    1.16 -(* new locales *)
    1.17 -
    1.18 -fun locale_extern new_locale x = 
    1.19 -  if new_locale then Locale.extern x else Old_Locale.extern x;
    1.20 -fun locale_add_type_syntax new_locale x =
    1.21 -  if new_locale then Locale.add_type_syntax x else Old_Locale.add_type_syntax x;
    1.22 -fun locale_add_term_syntax new_locale x =
    1.23 -  if new_locale then Locale.add_term_syntax x else Old_Locale.add_term_syntax x;
    1.24 -fun locale_add_declaration new_locale x =
    1.25 -  if new_locale then Locale.add_declaration x else Old_Locale.add_declaration x;
    1.26 -fun locale_add_thmss new_locale x =
    1.27 -  if new_locale then Locale.add_thmss x else Old_Locale.add_thmss x;
    1.28 -fun locale_init new_locale x =
    1.29 -  if new_locale then Locale.init x else Old_Locale.init x;
    1.30 -fun locale_intern new_locale x =
    1.31 -  if new_locale then Locale.intern x else Old_Locale.intern x;
    1.32 -
    1.33  (* context data *)
    1.34  
    1.35 -datatype target = Target of {target: string, new_locale: bool, is_locale: bool,
    1.36 +datatype target = Target of {target: string, is_locale: bool,
    1.37    is_class: bool, instantiation: string list * (string * sort) list * sort,
    1.38    overloading: (string * (string * typ) * bool) list};
    1.39  
    1.40 -fun make_target target new_locale is_locale is_class instantiation overloading =
    1.41 -  Target {target = target, new_locale = new_locale, is_locale = is_locale,
    1.42 +fun make_target target is_locale is_class instantiation overloading =
    1.43 +  Target {target = target, is_locale = is_locale,
    1.44      is_class = is_class, instantiation = instantiation, overloading = overloading};
    1.45  
    1.46 -val global_target = make_target "" false false false ([], [], []) [];
    1.47 +val global_target = make_target "" false false ([], [], []) [];
    1.48  
    1.49  structure Data = ProofDataFun
    1.50  (
    1.51 @@ -64,7 +47,7 @@
    1.52  fun pretty_thy ctxt target is_locale is_class =
    1.53    let
    1.54      val thy = ProofContext.theory_of ctxt;
    1.55 -    val target_name = (if is_class then "class " else "locale ") ^ locale_extern is_class thy target;
    1.56 +    val target_name = (if is_class then "class " else "locale ") ^ Locale.extern thy target;
    1.57      val fixes = map (fn (x, T) => (Binding.name x, SOME T, NoSyn))
    1.58        (#1 (ProofContext.inferred_fixes ctxt));
    1.59      val assumes = map (fn A => (Attrib.empty_binding, [(Thm.term_of A, [])]))
    1.60 @@ -89,7 +72,7 @@
    1.61  
    1.62  (* target declarations *)
    1.63  
    1.64 -fun target_decl add (Target {target, new_locale, ...}) d lthy =
    1.65 +fun target_decl add (Target {target, ...}) d lthy =
    1.66    let
    1.67      val d' = Morphism.transform (LocalTheory.target_morphism lthy) d;
    1.68      val d0 = Morphism.form d';
    1.69 @@ -100,12 +83,12 @@
    1.70        |> LocalTheory.target (Context.proof_map d0)
    1.71      else
    1.72        lthy
    1.73 -      |> LocalTheory.target (add new_locale target d')
    1.74 +      |> LocalTheory.target (add target d')
    1.75    end;
    1.76  
    1.77 -val type_syntax = target_decl locale_add_type_syntax;
    1.78 -val term_syntax = target_decl locale_add_term_syntax;
    1.79 -val declaration = target_decl locale_add_declaration;
    1.80 +val type_syntax = target_decl Locale.add_type_syntax;
    1.81 +val term_syntax = target_decl Locale.add_term_syntax;
    1.82 +val declaration = target_decl Locale.add_declaration;
    1.83  
    1.84  fun class_target (Target {target, ...}) f =
    1.85    LocalTheory.raw_theory f #>
    1.86 @@ -166,7 +149,7 @@
    1.87    |> ProofContext.note_thmss_i kind facts
    1.88    ||> ProofContext.restore_naming ctxt;
    1.89  
    1.90 -fun notes (Target {target, is_locale, new_locale, ...}) kind facts lthy =
    1.91 +fun notes (Target {target, is_locale, ...}) kind facts lthy =
    1.92    let
    1.93      val thy = ProofContext.theory_of lthy;
    1.94      val facts' = facts
    1.95 @@ -185,7 +168,7 @@
    1.96          #> PureThy.note_thmss_grouped kind (LocalTheory.group_of lthy) global_facts #> snd
    1.97          #> Sign.restore_naming thy)
    1.98      |> not is_locale ? LocalTheory.target (note_local kind global_facts #> snd)
    1.99 -    |> is_locale ? LocalTheory.target (locale_add_thmss new_locale target kind target_facts)
   1.100 +    |> is_locale ? LocalTheory.target (Locale.add_thmss target kind target_facts)
   1.101      |> note_local kind local_facts
   1.102    end;
   1.103  
   1.104 @@ -313,7 +296,7 @@
   1.105            (fn name => fn (Const (c, _), rhs) => Overloading.define checked name (c, rhs))
   1.106        | NONE =>
   1.107            if is_none (Class_Target.instantiation_param lthy c)
   1.108 -          then (fn name => fn eq => Thm.add_def false false (name, Logic.mk_equals eq))
   1.109 +          then (fn name => fn eq => Thm.add_def false false (Binding.name name, Logic.mk_equals eq))
   1.110            else (fn name => fn (Const (c, _), rhs) => AxClass.define_overloaded name (c, rhs)));
   1.111      val (global_def, lthy3) = lthy2
   1.112        |> LocalTheory.theory_result (define_const (Binding.base_name name') (lhs', rhs'));
   1.113 @@ -335,13 +318,13 @@
   1.114  fun init_target _ NONE = global_target
   1.115    | init_target thy (SOME target) =
   1.116        make_target target (Locale.defined thy (Locale.intern thy target))
   1.117 -      true (Class_Target.is_class thy target) ([], [], []) [];
   1.118 +      (Class_Target.is_class thy target) ([], [], []) [];
   1.119  
   1.120 -fun init_ctxt (Target {target, new_locale, is_locale, is_class, instantiation, overloading}) =
   1.121 +fun init_ctxt (Target {target, is_locale, is_class, instantiation, overloading}) =
   1.122    if not (null (#1 instantiation)) then Class_Target.init_instantiation instantiation
   1.123    else if not (null overloading) then Overloading.init overloading
   1.124    else if not is_locale then ProofContext.init
   1.125 -  else if not is_class then locale_init new_locale target
   1.126 +  else if not is_class then Locale.init target
   1.127    else Class_Target.init target;
   1.128  
   1.129  fun init_lthy (ta as Target {target, instantiation, overloading, ...}) =
   1.130 @@ -375,7 +358,7 @@
   1.131      val ctxt = ProofContext.init thy;
   1.132      val ops = raw_ops |> map (fn (name, const, checked) =>
   1.133        (name, Term.dest_Const (prep_const ctxt const), checked));
   1.134 -  in thy |> init_lthy_ctxt (make_target "" false false false ([], [], []) ops) end;
   1.135 +  in thy |> init_lthy_ctxt (make_target "" false false ([], [], []) ops) end;
   1.136  
   1.137  in
   1.138  
   1.139 @@ -383,10 +366,9 @@
   1.140  fun begin target ctxt = init_lthy (init_target (ProofContext.theory_of ctxt) (SOME target)) ctxt;
   1.141  
   1.142  fun context "-" thy = init NONE thy
   1.143 -  | context target thy = init (SOME (locale_intern
   1.144 -      (Locale.defined thy (Locale.intern thy target)) thy target)) thy;
   1.145 +  | context target thy = init (SOME (Locale.intern thy target)) thy;
   1.146  
   1.147 -fun instantiation arities = init_lthy_ctxt (make_target "" false false false arities []);
   1.148 +fun instantiation arities = init_lthy_ctxt (make_target "" false false arities []);
   1.149  fun instantiation_cmd raw_arities thy =
   1.150    instantiation (read_multi_arity thy raw_arities) thy;
   1.151