# HG changeset patch
# User wenzelm
# Date 1305383267 -7200
# Node ID 4b660cdab9b71f597a9471fbfa492efe82ab20ab
# Parent  a6dafa3d7adaaf2b98cb6bbe36975de1aed4eb0c
modernized structure Rule_Insts;

diff -r a6dafa3d7ada -r 4b660cdab9b7 src/HOL/Nominal/nominal_fresh_fun.ML
--- a/src/HOL/Nominal/nominal_fresh_fun.ML	Sat May 14 16:22:53 2011 +0200
+++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Sat May 14 16:27:47 2011 +0200
@@ -34,7 +34,7 @@
   gen_res_inst_tac_term (K Drule.cterm_instantiate) [];
 
 fun cut_inst_tac_term' tinst th =
-  res_inst_tac_term' tinst false (RuleInsts.make_elim_preserve th);
+  res_inst_tac_term' tinst false (Rule_Insts.make_elim_preserve th);
 
 fun get_dyn_thm thy name atom_name =
   Global_Theory.get_thm thy name handle ERROR _ =>
diff -r a6dafa3d7ada -r 4b660cdab9b7 src/Pure/Isar/rule_insts.ML
--- a/src/Pure/Isar/rule_insts.ML	Sat May 14 16:22:53 2011 +0200
+++ b/src/Pure/Isar/rule_insts.ML	Sat May 14 16:27:47 2011 +0200
@@ -26,7 +26,7 @@
   val make_elim_preserve: thm -> thm
 end;
 
-structure RuleInsts: RULE_INSTS =
+structure Rule_Insts: RULE_INSTS =
 struct
 
 (** reading instantiations **)
@@ -422,5 +422,5 @@
 
 end;
 
-structure Basic_Rule_Insts: BASIC_RULE_INSTS = RuleInsts;
+structure Basic_Rule_Insts: BASIC_RULE_INSTS = Rule_Insts;
 open Basic_Rule_Insts;