tuned signature;
authorwenzelm
Sun Feb 18 15:05:21 2018 +0100 (17 months ago)
changeset 676491e1782c1aedf
parent 67648 f6e351043014
child 67650 5e4f9a0ffea5
tuned signature;
src/HOL/Decision_Procs/Commutative_Ring.thy
src/HOL/Decision_Procs/Reflective_Field.thy
src/HOL/Library/conditional_parametricity.ML
src/HOL/Probability/Giry_Monad.thy
src/HOL/Tools/Function/function_context_tree.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/lin_arith.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/classical.ML
src/Provers/splitter.ML
src/Pure/Isar/code.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/spec_rules.ML
src/Pure/Isar/subgoal.ML
src/Pure/Proof/proof_syntax.ML
src/Pure/Proof/reconstruct.ML
src/Pure/Tools/named_theorems.ML
src/Pure/facts.ML
src/Pure/more_thm.ML
src/Pure/raw_simplifier.ML
src/Pure/thm.ML
src/Tools/Code/code_runtime.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Sat Feb 17 20:03:37 2018 +0100
     1.2 +++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Sun Feb 18 15:05:21 2018 +0100
     1.3 @@ -737,7 +737,7 @@
     1.4    (case get_matching_rules ctxt (Ring_Simps.get (Context.Proof ctxt)) t of
     1.5       SOME (ths1, ths2, ths3, ths4, th5, th) =>
     1.6         let val tr =
     1.7 -         Thm.transfer (Proof_Context.theory_of ctxt) #>
     1.8 +         Thm.transfer' ctxt #>
     1.9           (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
    1.10         in (map tr ths1, map tr ths2, map tr ths3, map tr ths4, tr th5, tr th) end
    1.11     | NONE => error "get_ring_simps: lookup failed");
     2.1 --- a/src/HOL/Decision_Procs/Reflective_Field.thy	Sat Feb 17 20:03:37 2018 +0100
     2.2 +++ b/src/HOL/Decision_Procs/Reflective_Field.thy	Sun Feb 18 15:05:21 2018 +0100
     2.3 @@ -757,7 +757,7 @@
     2.4    (case get_matching_rules ctxt (Field_Simps.get (Context.Proof ctxt)) t of
     2.5       SOME (ths1, ths2, ths3, th4, th) =>
     2.6         let val tr =
     2.7 -         Thm.transfer (Proof_Context.theory_of ctxt) #>
     2.8 +         Thm.transfer' ctxt #>
     2.9           (case optcT of NONE => I | SOME cT => inst [cT] [] #> norm)
    2.10         in (map tr ths1, map tr ths2, map tr ths3, tr th4, tr th) end
    2.11     | NONE => error "get_field_simps: lookup failed");
     3.1 --- a/src/HOL/Library/conditional_parametricity.ML	Sat Feb 17 20:03:37 2018 +0100
     3.2 +++ b/src/HOL/Library/conditional_parametricity.ML	Sun Feb 18 15:05:21 2018 +0100
     3.3 @@ -457,7 +457,7 @@
     3.4        Option.filter (is_parametricity_theorem andf (not o curry Term.could_unify
     3.5          (Thm.full_prop_of @{thm is_equality_Rel})) o Thm.full_prop_of) o preprocess_theorem ctxt;
     3.6    in
     3.7 -    map_filter (parametricity_thm_map_filter o Thm.transfer (Proof_Context.theory_of ctxt))
     3.8 +    map_filter (parametricity_thm_map_filter o Thm.transfer' ctxt)
     3.9        (Transfer.get_transfer_raw ctxt)
    3.10    end;
    3.11  
     4.1 --- a/src/HOL/Probability/Giry_Monad.thy	Sat Feb 17 20:03:37 2018 +0100
     4.2 +++ b/src/HOL/Probability/Giry_Monad.thy	Sun Feb 18 15:05:21 2018 +0100
     4.3 @@ -194,7 +194,7 @@
     4.4  
     4.5  fun subprob_cong thm ctxt = (
     4.6    let
     4.7 -    val thm' = Thm.transfer (Proof_Context.theory_of ctxt) thm
     4.8 +    val thm' = Thm.transfer' ctxt thm
     4.9      val free = thm' |> Thm.concl_of |> HOLogic.dest_Trueprop |> dest_comb |> fst |>
    4.10        dest_comb |> snd |> strip_abs_body |> head_of |> is_Free
    4.11    in
     5.1 --- a/src/HOL/Tools/Function/function_context_tree.ML	Sat Feb 17 20:03:37 2018 +0100
     5.2 +++ b/src/HOL/Tools/Function/function_context_tree.ML	Sun Feb 18 15:05:21 2018 +0100
     5.3 @@ -53,7 +53,7 @@
     5.4  
     5.5  fun get_function_congs ctxt =
     5.6    FunctionCongs.get (Context.Proof ctxt)
     5.7 -  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
     5.8 +  |> map (Thm.transfer' ctxt);
     5.9  
    5.10  val add_function_cong = FunctionCongs.map o Thm.add_thm o Thm.trim_context;
    5.11  
     6.1 --- a/src/HOL/Tools/inductive.ML	Sat Feb 17 20:03:37 2018 +0100
     6.2 +++ b/src/HOL/Tools/inductive.ML	Sun Feb 18 15:05:21 2018 +0100
     6.3 @@ -276,7 +276,7 @@
     6.4  
     6.5  fun get_monos ctxt =
     6.6    #monos (rep_data ctxt)
     6.7 -  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
     6.8 +  |> map (Thm.transfer' ctxt);
     6.9  
    6.10  fun mk_mono ctxt thm =
    6.11    let
    6.12 @@ -314,7 +314,7 @@
    6.13  
    6.14  fun retrieve_equations ctxt =
    6.15    Item_Net.retrieve (#equations (rep_data ctxt))
    6.16 -  #> map (Thm.transfer (Proof_Context.theory_of ctxt));
    6.17 +  #> map (Thm.transfer' ctxt);
    6.18  
    6.19  val equation_add_permissive =
    6.20    Thm.declaration_attribute (fn thm =>
     7.1 --- a/src/HOL/Tools/lin_arith.ML	Sat Feb 17 20:03:37 2018 +0100
     7.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Feb 18 15:05:21 2018 +0100
     7.3 @@ -87,7 +87,7 @@
     7.4  
     7.5  fun get_splits ctxt =
     7.6    #splits (get_arith_data ctxt)
     7.7 -  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
     7.8 +  |> map (Thm.transfer' ctxt);
     7.9  
    7.10  fun add_split thm = Lin_Arith_Data.map (fn {splits, inj_consts, discrete} =>
    7.11    {splits = update Thm.eq_thm_prop (Thm.trim_context thm) splits,
     8.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sat Feb 17 20:03:37 2018 +0100
     8.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Feb 18 15:05:21 2018 +0100
     8.3 @@ -149,7 +149,7 @@
     8.4  val map_data = Data.map;
     8.5  val get_data = Data.get o Context.Proof;
     8.6  
     8.7 -fun get_neqE ctxt = map (Thm.transfer (Proof_Context.theory_of ctxt)) (#neqE (get_data ctxt));
     8.8 +fun get_neqE ctxt = map (Thm.transfer' ctxt) (#neqE (get_data ctxt));
     8.9  
    8.10  fun map_inj_thms f {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset, number_of} =
    8.11    {add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms, inj_thms = f inj_thms,
     9.1 --- a/src/Provers/classical.ML	Sat Feb 17 20:03:37 2018 +0100
     9.2 +++ b/src/Provers/classical.ML	Sun Feb 18 15:05:21 2018 +0100
     9.3 @@ -196,7 +196,7 @@
     9.4    trying rules in order. *)
     9.5  fun swap_res_tac ctxt rls =
     9.6    let
     9.7 -    val transfer = Thm.transfer (Proof_Context.theory_of ctxt);
     9.8 +    val transfer = Thm.transfer' ctxt;
     9.9      fun addrl rl brls = (false, transfer rl) :: (true, transfer rl RSN (2, Data.swap)) :: brls;
    9.10    in
    9.11      assume_tac ctxt ORELSE'
    10.1 --- a/src/Provers/splitter.ML	Sat Feb 17 20:03:37 2018 +0100
    10.2 +++ b/src/Provers/splitter.ML	Sun Feb 18 15:05:21 2018 +0100
    10.3 @@ -440,7 +440,7 @@
    10.4      val (name, asm) = split_thm_info split
    10.5      val split0 = Thm.trim_context split
    10.6      fun tac ctxt' =
    10.7 -      let val split' = Thm.transfer (Proof_Context.theory_of ctxt') split0 in
    10.8 +      let val split' = Thm.transfer' ctxt' split0 in
    10.9          (if asm then split_asm_tac ctxt' [split']
   10.10           else if bang
   10.11                then split_tac ctxt' [split'] THEN_ALL_NEW
    11.1 --- a/src/Pure/Isar/code.ML	Sat Feb 17 20:03:37 2018 +0100
    11.2 +++ b/src/Pure/Isar/code.ML	Sun Feb 18 15:05:21 2018 +0100
    11.3 @@ -1105,7 +1105,7 @@
    11.4    singleton (Variable.trade (K (map (Conv.fconv_rule (conv (Simplifier.rewrite ctxt))))) ctxt)
    11.5  
    11.6  fun preprocess conv ctxt =
    11.7 -  Thm.transfer (Proof_Context.theory_of ctxt)
    11.8 +  Thm.transfer' ctxt
    11.9    #> rewrite_eqn conv ctxt
   11.10    #> Axclass.unoverload ctxt;
   11.11  
    12.1 --- a/src/Pure/Isar/context_rules.ML	Sat Feb 17 20:03:37 2018 +0100
    12.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Feb 18 15:05:21 2018 +0100
    12.3 @@ -161,7 +161,7 @@
    12.4  
    12.5  fun find_rules_netpair ctxt weighted facts goal (inet, enet) =
    12.6    find_erules weighted facts enet @ find_irules weighted goal inet
    12.7 -  |> map (Thm.transfer (Proof_Context.theory_of ctxt));
    12.8 +  |> map (Thm.transfer' ctxt);
    12.9  
   12.10  fun find_rules ctxt weighted facts goal =
   12.11    map (find_rules_netpair ctxt weighted facts goal) (netpairs ctxt);
    13.1 --- a/src/Pure/Isar/locale.ML	Sat Feb 17 20:03:37 2018 +0100
    13.2 +++ b/src/Pure/Isar/locale.ML	Sun Feb 18 15:05:21 2018 +0100
    13.3 @@ -648,8 +648,7 @@
    13.4  );
    13.5  
    13.6  fun get_thms which ctxt =
    13.7 -  map (Thm.transfer (Proof_Context.theory_of ctxt))
    13.8 -    (which (Thms.get (Context.Proof ctxt)));
    13.9 +  map (Thm.transfer' ctxt) (which (Thms.get (Context.Proof ctxt)));
   13.10  
   13.11  val get_witnesses = get_thms #1;
   13.12  val get_intros = get_thms #2;
    14.1 --- a/src/Pure/Isar/spec_rules.ML	Sat Feb 17 20:03:37 2018 +0100
    14.2 +++ b/src/Pure/Isar/spec_rules.ML	Sun Feb 18 15:05:21 2018 +0100
    14.3 @@ -57,7 +57,7 @@
    14.4  
    14.5  fun retrieve_generic context =
    14.6    Item_Net.retrieve (Rules.get context)
    14.7 -  #> (map o apsnd o apsnd o map) (Thm.transfer (Context.theory_of context));
    14.8 +  #> (map o apsnd o apsnd o map) (Thm.transfer'' context);
    14.9  
   14.10  val retrieve = retrieve_generic o Context.Proof;
   14.11  val retrieve_global = retrieve_generic o Context.Theory;
    15.1 --- a/src/Pure/Isar/subgoal.ML	Sat Feb 17 20:03:37 2018 +0100
    15.2 +++ b/src/Pure/Isar/subgoal.ML	Sun Feb 18 15:05:21 2018 +0100
    15.3 @@ -44,7 +44,7 @@
    15.4  fun gen_focus (do_prems, do_concl) ctxt i bindings raw_st =
    15.5    let
    15.6      val st = raw_st
    15.7 -      |> Thm.transfer (Proof_Context.theory_of ctxt)
    15.8 +      |> Thm.transfer' ctxt
    15.9        |> Raw_Simplifier.norm_hhf_protect ctxt;
   15.10      val ((schematic_types, [st']), ctxt1) = Variable.importT [st] ctxt;
   15.11      val ((params, goal), ctxt2) = Variable.focus_cterm bindings (Thm.cprem_of st' i) ctxt1;
    16.1 --- a/src/Pure/Proof/proof_syntax.ML	Sat Feb 17 20:03:37 2018 +0100
    16.2 +++ b/src/Pure/Proof/proof_syntax.ML	Sun Feb 18 15:05:21 2018 +0100
    16.3 @@ -244,7 +244,7 @@
    16.4  
    16.5  fun proof_of ctxt full raw_thm =
    16.6    let
    16.7 -    val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm;
    16.8 +    val thm = Thm.transfer' ctxt raw_thm;
    16.9      val prop = Thm.full_prop_of thm;
   16.10      val prf = Thm.proof_of thm;
   16.11      val prf' =
    17.1 --- a/src/Pure/Proof/reconstruct.ML	Sat Feb 17 20:03:37 2018 +0100
    17.2 +++ b/src/Pure/Proof/reconstruct.ML	Sun Feb 18 15:05:21 2018 +0100
    17.3 @@ -332,7 +332,7 @@
    17.4  val prop_of = prop_of' [];
    17.5  
    17.6  fun proof_of ctxt raw_thm =
    17.7 -  let val thm = Thm.transfer (Proof_Context.theory_of ctxt) raw_thm
    17.8 +  let val thm = Thm.transfer' ctxt raw_thm
    17.9    in reconstruct_proof ctxt (Thm.prop_of thm) (Thm.proof_of thm) end;
   17.10  
   17.11  
    18.1 --- a/src/Pure/Tools/named_theorems.ML	Sat Feb 17 20:03:37 2018 +0100
    18.2 +++ b/src/Pure/Tools/named_theorems.ML	Sun Feb 18 15:05:21 2018 +0100
    18.3 @@ -52,7 +52,7 @@
    18.4  fun member ctxt = Item_Net.member o the_entry (Context.Proof ctxt);
    18.5  
    18.6  fun content context =
    18.7 -  rev o map (Thm.transfer (Context.theory_of context)) o Item_Net.content o the_entry context;
    18.8 +  rev o map (Thm.transfer'' context) o Item_Net.content o the_entry context;
    18.9  
   18.10  val get = content o Context.Proof;
   18.11  
    19.1 --- a/src/Pure/facts.ML	Sat Feb 17 20:03:37 2018 +0100
    19.2 +++ b/src/Pure/facts.ML	Sun Feb 18 15:05:21 2018 +0100
    19.3 @@ -195,7 +195,7 @@
    19.4    in
    19.5     {name = name,
    19.6      dynamic = dynamic,
    19.7 -    thms = map (Thm.transfer (Context.theory_of context)) thms}
    19.8 +    thms = map (Thm.transfer'' context) thms}
    19.9    end;
   19.10  
   19.11  
    20.1 --- a/src/Pure/more_thm.ML	Sat Feb 17 20:03:37 2018 +0100
    20.2 +++ b/src/Pure/more_thm.ML	Sun Feb 18 15:05:21 2018 +0100
    20.3 @@ -617,7 +617,7 @@
    20.4    let val (x', th') = f (x, th) in (SOME x', SOME th') end;
    20.5  
    20.6  fun apply_attribute (att: attribute) th x =
    20.7 -  let val (x', th') = att (x, check_hyps x (Thm.transfer (Context.theory_of x) th))
    20.8 +  let val (x', th') = att (x, check_hyps x (Thm.transfer'' x th))
    20.9    in (the_default th th', the_default x x') end;
   20.10  
   20.11  fun attribute_declaration att th x = #2 (apply_attribute att th x);
   20.12 @@ -685,7 +685,7 @@
   20.13      val show_hyps = Config.get ctxt show_hyps;
   20.14  
   20.15      val th = raw_th
   20.16 -      |> perhaps (try (Thm.transfer (Proof_Context.theory_of ctxt)))
   20.17 +      |> perhaps (try (Thm.transfer' ctxt))
   20.18        |> perhaps (try Thm.strip_shyps);
   20.19  
   20.20      val hyps = if show_hyps then Thm.hyps_of th else undeclared_hyps (Context.Proof ctxt) th;
    21.1 --- a/src/Pure/raw_simplifier.ML	Sat Feb 17 20:03:37 2018 +0100
    21.2 +++ b/src/Pure/raw_simplifier.ML	Sun Feb 18 15:05:21 2018 +0100
    21.3 @@ -579,8 +579,7 @@
    21.4  local
    21.5  
    21.6  fun comb_simps ctxt comb mk_rrule thms =
    21.7 -  let
    21.8 -    val rews = extract_rews ctxt (map (Thm.transfer (Proof_Context.theory_of ctxt)) thms);
    21.9 +  let val rews = extract_rews ctxt (map (Thm.transfer' ctxt) thms);
   21.10    in fold (fold comb o mk_rrule) rews ctxt end;
   21.11  
   21.12  in
   21.13 @@ -1388,7 +1387,7 @@
   21.14  local
   21.15  
   21.16  fun gen_norm_hhf ss ctxt =
   21.17 -  Thm.transfer (Proof_Context.theory_of ctxt) #>
   21.18 +  Thm.transfer' ctxt #>
   21.19    (fn th =>
   21.20      if Drule.is_norm_hhf (Thm.prop_of th) then th
   21.21      else
    22.1 --- a/src/Pure/thm.ML	Sat Feb 17 20:03:37 2018 +0100
    22.2 +++ b/src/Pure/thm.ML	Sun Feb 18 15:05:21 2018 +0100
    22.3 @@ -79,6 +79,8 @@
    22.4    val trim_context: thm -> thm
    22.5    val transfer_cterm: theory -> cterm -> cterm
    22.6    val transfer: theory -> thm -> thm
    22.7 +  val transfer': Proof.context -> thm -> thm
    22.8 +  val transfer'': Context.generic -> thm -> thm
    22.9    val renamed_prop: term -> thm -> thm
   22.10    val weaken: cterm -> thm -> thm
   22.11    val weaken_sorts: sort list -> cterm -> cterm
   22.12 @@ -457,6 +459,9 @@
   22.13          prop = prop})
   22.14    end;
   22.15  
   22.16 +val transfer' = transfer o Proof_Context.theory_of;
   22.17 +val transfer'' = transfer o Context.theory_of;
   22.18 +
   22.19  
   22.20  (* matching *)
   22.21  
    23.1 --- a/src/Tools/Code/code_runtime.ML	Sat Feb 17 20:03:37 2018 +0100
    23.2 +++ b/src/Tools/Code/code_runtime.ML	Sun Feb 18 15:05:21 2018 +0100
    23.3 @@ -354,7 +354,7 @@
    23.4  
    23.5  fun get ctxt =
    23.6    Computation_Preproc_Data.get (Proof_Context.theory_of ctxt)
    23.7 -  |> map (Thm.transfer (Proof_Context.theory_of ctxt))
    23.8 +  |> map (Thm.transfer' ctxt)
    23.9  
   23.10  in
   23.11  
    24.1 --- a/src/Tools/induct.ML	Sat Feb 17 20:03:37 2018 +0100
    24.2 +++ b/src/Tools/induct.ML	Sun Feb 18 15:05:21 2018 +0100
    24.3 @@ -277,11 +277,11 @@
    24.4  
    24.5  fun lookup_rule which ctxt =
    24.6    AList.lookup (op =) (Item_Net.content (which (get_local ctxt)))
    24.7 -  #> Option.map (Thm.transfer (Proof_Context.theory_of ctxt));
    24.8 +  #> Option.map (Thm.transfer' ctxt);
    24.9  
   24.10  fun find_rules which how ctxt x =
   24.11    Item_Net.retrieve (which (get_local ctxt)) (how x)
   24.12 -  |> map (Thm.transfer (Proof_Context.theory_of ctxt) o snd);
   24.13 +  |> map (Thm.transfer' ctxt o snd);
   24.14  
   24.15  in
   24.16