uniform Local_Theory.declaration with explicit params;
authorwenzelm
Fri Oct 28 22:17:30 2011 +0200 (2011-10-28)
changeset 4529157cd50f98fdc
parent 45290 f599ac41e7f5
child 45292 90106a351a11
uniform Local_Theory.declaration with explicit params;
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Function/function.ML
src/HOL/Tools/Quotient/quotient_def.ML
src/HOL/Tools/Quotient/quotient_typ.ML
src/HOL/Tools/enriched_type.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/typedef.ML
src/Pure/Isar/class.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/named_target.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/spec_rules.ML
src/Pure/simplifier.ML
     1.1 --- a/src/HOL/Statespace/state_space.ML	Fri Oct 28 17:15:52 2011 +0200
     1.2 +++ b/src/HOL/Statespace/state_space.ML	Fri Oct 28 22:17:30 2011 +0200
     1.3 @@ -340,7 +340,7 @@
     1.4  fun add_declaration name decl thy =
     1.5    thy
     1.6    |> Named_Target.init I name
     1.7 -  |> (fn lthy => Local_Theory.declaration false (decl lthy) lthy)
     1.8 +  |> (fn lthy => Local_Theory.declaration {syntax = false, pervasive = false} (decl lthy) lthy)
     1.9    |> Local_Theory.exit_global;
    1.10  
    1.11  fun parent_components thy (Ts, pname, renaming) =
     2.1 --- a/src/HOL/Tools/Function/function.ML	Fri Oct 28 17:15:52 2011 +0200
     2.2 +++ b/src/HOL/Tools/Function/function.ML	Fri Oct 28 22:17:30 2011 +0200
     2.3 @@ -128,7 +128,8 @@
     2.4          val _ = Proof_Display.print_consts do_print lthy (K false) (map fst fixes)
     2.5        in
     2.6          (info,
     2.7 -         lthy |> Local_Theory.declaration false (add_function_data o transform_function_data info))
     2.8 +         lthy |> Local_Theory.declaration {syntax = false, pervasive = false}
     2.9 +          (add_function_data o transform_function_data info))
    2.10        end
    2.11    in
    2.12      ((goal_state, afterqed), lthy')
    2.13 @@ -203,7 +204,8 @@
    2.14              in
    2.15                (info',
    2.16                 lthy 
    2.17 -               |> Local_Theory.declaration false (add_function_data o transform_function_data info')
    2.18 +               |> Local_Theory.declaration {syntax = false, pervasive = false}
    2.19 +                 (add_function_data o transform_function_data info')
    2.20                 |> Spec_Rules.add Spec_Rules.Equational (fs, tsimps))
    2.21              end)
    2.22          end
     3.1 --- a/src/HOL/Tools/Quotient/quotient_def.ML	Fri Oct 28 17:15:52 2011 +0200
     3.2 +++ b/src/HOL/Tools/Quotient/quotient_def.ML	Fri Oct 28 22:17:30 2011 +0200
     3.3 @@ -75,7 +75,7 @@
     3.4      fun qcinfo phi = Quotient_Info.transform_quotconsts phi qconst_data
     3.5      fun trans_name phi = (fst o dest_Const o #qconst) (qcinfo phi)
     3.6      val lthy'' =
     3.7 -      Local_Theory.declaration true
     3.8 +      Local_Theory.declaration {syntax = false, pervasive = true}
     3.9          (fn phi => Quotient_Info.update_quotconsts (trans_name phi) (qcinfo phi)) lthy'
    3.10    in
    3.11      (qconst_data, lthy'')
     4.1 --- a/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Oct 28 17:15:52 2011 +0200
     4.2 +++ b/src/HOL/Tools/Quotient/quotient_typ.ML	Fri Oct 28 22:17:30 2011 +0200
     4.3 @@ -143,7 +143,7 @@
     4.4      fun qinfo phi = Quotient_Info.transform_quotients phi quotients
     4.5  
     4.6      val lthy4 = lthy3
     4.7 -      |> Local_Theory.declaration true
     4.8 +      |> Local_Theory.declaration {syntax = false, pervasive = true}
     4.9          (fn phi => Quotient_Info.update_quotients qty_full_name (qinfo phi))
    4.10        |> (snd oo Local_Theory.note)
    4.11          ((equiv_thm_name,
     5.1 --- a/src/HOL/Tools/enriched_type.ML	Fri Oct 28 17:15:52 2011 +0200
     5.2 +++ b/src/HOL/Tools/enriched_type.ML	Fri Oct 28 22:17:30 2011 +0200
     5.3 @@ -240,7 +240,8 @@
     5.4          |> Local_Theory.note ((qualify identityN, []),
     5.5              [prove_identity lthy id_thm])
     5.6          |> snd
     5.7 -        |> Local_Theory.declaration false (mapper_declaration comp_thm id_thm))
     5.8 +        |> Local_Theory.declaration {syntax = false, pervasive = false}
     5.9 +          (mapper_declaration comp_thm id_thm))
    5.10    in
    5.11      lthy
    5.12      |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) [comp_prop, id_prop])
     6.1 --- a/src/HOL/Tools/inductive.ML	Fri Oct 28 17:15:52 2011 +0200
     6.2 +++ b/src/HOL/Tools/inductive.ML	Fri Oct 28 22:17:30 2011 +0200
     6.3 @@ -931,7 +931,7 @@
     6.4         eqs = eqs'};
     6.5  
     6.6      val lthy4 = lthy3
     6.7 -      |> Local_Theory.declaration false (fn phi =>
     6.8 +      |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi =>
     6.9          let val result' = transform_result phi result;
    6.10          in put_inductives cnames (*global names!?*) ({names = cnames, coind = coind}, result') end);
    6.11    in (result, lthy4) end;
     7.1 --- a/src/HOL/Tools/typedef.ML	Fri Oct 28 17:15:52 2011 +0200
     7.2 +++ b/src/HOL/Tools/typedef.ML	Fri Oct 28 22:17:30 2011 +0200
     7.3 @@ -247,7 +247,8 @@
     7.4            Abs_cases = Abs_cases, Rep_induct = Rep_induct, Abs_induct = Abs_induct});
     7.5        in
     7.6          lthy2
     7.7 -        |> Local_Theory.declaration true (fn phi => put_info full_tname (transform_info phi info))
     7.8 +        |> Local_Theory.declaration {syntax = false, pervasive = true}
     7.9 +          (fn phi => put_info full_tname (transform_info phi info))
    7.10          |> Local_Theory.background_theory (Typedef_Interpretation.data full_tname)
    7.11          |> pair (full_tname, info)
    7.12        end;
     8.1 --- a/src/Pure/Isar/class.ML	Fri Oct 28 17:15:52 2011 +0200
     8.2 +++ b/src/Pure/Isar/class.ML	Fri Oct 28 22:17:30 2011 +0200
     8.3 @@ -561,7 +561,6 @@
     8.4            (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
     8.5              Generic_Target.theory_abbrev prmode ((b, mx), t)),
     8.6          declaration = K Generic_Target.theory_declaration,
     8.7 -        syntax_declaration = K Generic_Target.theory_declaration,
     8.8          pretty = pretty,
     8.9          exit = Local_Theory.target_of o conclude}
    8.10    end;
     9.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Oct 28 17:15:52 2011 +0200
     9.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Oct 28 22:17:30 2011 +0200
     9.3 @@ -202,9 +202,8 @@
     9.4    ML_Lex.read pos txt
     9.5    |> ML_Context.expression pos
     9.6      "val declaration: Morphism.declaration"
     9.7 -    ("Context.map_proof (Local_Theory." ^
     9.8 -      (if syntax then "syntax_declaration" else "declaration") ^ " " ^
     9.9 -      Bool.toString pervasive ^ " declaration)")
    9.10 +    ("Context.map_proof (Local_Theory.declaration {syntax = " ^ Bool.toString syntax ^ ", \
    9.11 +      \pervasive = " ^ Bool.toString pervasive ^ "} declaration)")
    9.12    |> Context.proof_map;
    9.13  
    9.14  
    10.1 --- a/src/Pure/Isar/local_theory.ML	Fri Oct 28 17:15:52 2011 +0200
    10.2 +++ b/src/Pure/Isar/local_theory.ML	Fri Oct 28 22:17:30 2011 +0200
    10.3 @@ -39,8 +39,7 @@
    10.4      local_theory -> (string * thm list) list * local_theory
    10.5    val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
    10.6      (term * term) * local_theory
    10.7 -  val declaration: bool -> declaration -> local_theory -> local_theory
    10.8 -  val syntax_declaration: bool -> declaration -> local_theory -> local_theory
    10.9 +  val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
   10.10    val pretty: local_theory -> Pretty.T list
   10.11    val set_defsort: sort -> local_theory -> local_theory
   10.12    val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> local_theory -> local_theory
   10.13 @@ -71,8 +70,7 @@
   10.14      local_theory -> (string * thm list) list * local_theory,
   10.15    abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
   10.16      (term * term) * local_theory,
   10.17 -  declaration: bool -> declaration -> local_theory -> local_theory,
   10.18 -  syntax_declaration: bool -> declaration -> local_theory -> local_theory,
   10.19 +  declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
   10.20    pretty: local_theory -> Pretty.T list,
   10.21    exit: local_theory -> Proof.context};
   10.22  
   10.23 @@ -200,7 +198,6 @@
   10.24  val define = apsnd checkpoint oo operation1 #define;
   10.25  val notes_kind = apsnd checkpoint ooo operation2 #notes;
   10.26  val declaration = checkpoint ooo operation2 #declaration;
   10.27 -val syntax_declaration = checkpoint ooo operation2 #syntax_declaration;
   10.28  
   10.29  
   10.30  
   10.31 @@ -210,24 +207,29 @@
   10.32  fun note (a, ths) = notes [(a, [(ths, [])])] #>> the_single;
   10.33  
   10.34  fun set_defsort S =
   10.35 -  syntax_declaration false (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
   10.36 +  declaration {syntax = true, pervasive = false}
   10.37 +    (K (Context.mapping (Sign.set_defsort S) (Proof_Context.set_defsort S)));
   10.38  
   10.39  
   10.40  (* notation *)
   10.41  
   10.42  fun type_notation add mode raw_args lthy =
   10.43 -  let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args
   10.44 -  in syntax_declaration false (Proof_Context.target_type_notation add mode args) lthy end;
   10.45 +  let val args = map (apfst (Morphism.typ (target_morphism lthy))) raw_args in
   10.46 +    declaration {syntax = true, pervasive = false}
   10.47 +      (Proof_Context.target_type_notation add mode args) lthy
   10.48 +  end;
   10.49  
   10.50  fun notation add mode raw_args lthy =
   10.51 -  let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args
   10.52 -  in syntax_declaration false (Proof_Context.target_notation add mode args) lthy end;
   10.53 +  let val args = map (apfst (Morphism.term (target_morphism lthy))) raw_args in
   10.54 +    declaration {syntax = true, pervasive = false}
   10.55 +      (Proof_Context.target_notation add mode args) lthy
   10.56 +  end;
   10.57  
   10.58  
   10.59  (* name space aliases *)
   10.60  
   10.61  fun alias global_alias local_alias b name =
   10.62 -  syntax_declaration false (fn phi =>
   10.63 +  declaration {syntax = true, pervasive = false} (fn phi =>
   10.64      let val b' = Morphism.binding phi b
   10.65      in Context.mapping (global_alias b' name) (local_alias b' name) end)
   10.66    #> local_alias b name;
    11.1 --- a/src/Pure/Isar/named_target.ML	Fri Oct 28 17:15:52 2011 +0200
    11.2 +++ b/src/Pure/Isar/named_target.ML	Fri Oct 28 22:17:30 2011 +0200
    11.3 @@ -56,9 +56,9 @@
    11.4      |> Local_Theory.target (add locale locale_decl)
    11.5    end;
    11.6  
    11.7 -fun target_declaration (Target {target, ...}) {syntax, pervasive} =
    11.8 +fun target_declaration (Target {target, ...}) params =
    11.9    if target = "" then Generic_Target.theory_declaration
   11.10 -  else locale_declaration target {syntax = syntax, pervasive = pervasive};
   11.11 +  else locale_declaration target params;
   11.12  
   11.13  
   11.14  (* consts in locales *)
   11.15 @@ -193,10 +193,7 @@
   11.16         {define = Generic_Target.define (target_foundation ta),
   11.17          notes = Generic_Target.notes (target_notes ta),
   11.18          abbrev = Generic_Target.abbrev (target_abbrev ta),
   11.19 -        declaration = fn pervasive => target_declaration ta
   11.20 -          {syntax = false, pervasive = pervasive},
   11.21 -        syntax_declaration = fn pervasive => target_declaration ta
   11.22 -          {syntax = true, pervasive = pervasive},
   11.23 +        declaration = target_declaration ta,
   11.24          pretty = pretty ta,
   11.25          exit = Local_Theory.target_of o before_exit}
   11.26    end;
    12.1 --- a/src/Pure/Isar/overloading.ML	Fri Oct 28 17:15:52 2011 +0200
    12.2 +++ b/src/Pure/Isar/overloading.ML	Fri Oct 28 22:17:30 2011 +0200
    12.3 @@ -207,7 +207,6 @@
    12.4            (fn prmode => fn (b, mx) => fn (t, _) => fn _ =>
    12.5              Generic_Target.theory_abbrev prmode ((b, mx), t)),
    12.6          declaration = K Generic_Target.theory_declaration,
    12.7 -        syntax_declaration = K Generic_Target.theory_declaration,
    12.8          pretty = pretty,
    12.9          exit = Local_Theory.target_of o conclude}
   12.10    end;
    13.1 --- a/src/Pure/Isar/spec_rules.ML	Fri Oct 28 17:15:52 2011 +0200
    13.2 +++ b/src/Pure/Isar/spec_rules.ML	Fri Oct 28 22:17:30 2011 +0200
    13.3 @@ -50,7 +50,7 @@
    13.4    let
    13.5      val cts = map (Thm.cterm_of (Proof_Context.theory_of lthy)) ts;
    13.6    in
    13.7 -    lthy |> Local_Theory.declaration true
    13.8 +    lthy |> Local_Theory.declaration {syntax = false, pervasive = true}
    13.9        (fn phi =>
   13.10          let
   13.11            val (ts', ths') =
    14.1 --- a/src/Pure/simplifier.ML	Fri Oct 28 17:15:52 2011 +0200
    14.2 +++ b/src/Pure/simplifier.ML	Fri Oct 28 22:17:30 2011 +0200
    14.3 @@ -192,7 +192,7 @@
    14.4         proc = proc,
    14.5         identifier = identifier};
    14.6    in
    14.7 -    lthy |> Local_Theory.declaration false (fn phi => fn context =>
    14.8 +    lthy |> Local_Theory.declaration {syntax = false, pervasive = false} (fn phi => fn context =>
    14.9        let
   14.10          val b' = Morphism.binding phi b;
   14.11          val simproc' = transform_simproc phi simproc;