modernized structure Rule_Insts;
authorwenzelm
Sat May 14 16:27:47 2011 +0200 (2011-05-14)
changeset 428064b660cdab9b7
parent 42805 a6dafa3d7ada
child 42807 e639d91d9073
modernized structure Rule_Insts;
src/HOL/Nominal/nominal_fresh_fun.ML
src/Pure/Isar/rule_insts.ML
     1.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat May 14 16:22:53 2011 +0200
     1.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat May 14 16:27:47 2011 +0200
     1.3 @@ -34,7 +34,7 @@
     1.4    gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
     1.5  
     1.6  fun cut_inst_tac_term' tinst th =
     1.7 -  res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
     1.8 +  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve th);
     1.9  
    1.10  fun get_dyn_thm thy name atom_name =
    1.11    Global_Theory.get_thm thy name handle ERROR _ =>
     2.1 --- a/src/Pure/Isar/rule_insts.ML	Sat May 14 16:22:53 2011 +0200
     2.2 +++ b/src/Pure/Isar/rule_insts.ML	Sat May 14 16:27:47 2011 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4    val make_elim_preserve: thm -> thm
     2.5  end;
     2.6  
     2.7 -structure RuleInsts: RULE_INSTS =
     2.8 +structure Rule_Insts: RULE_INSTS =
     2.9  struct
    2.10  
    2.11  (** reading instantiations **)
    2.12 @@ -422,5 +422,5 @@
    2.13  
    2.14  end;
    2.15  
    2.16 -structure Basic_Rule_Insts: BASIC_RULE_INSTS = RuleInsts;
    2.17 +structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
    2.18  open Basic_Rule_Insts;