# HG changeset patch
# User wenzelm
# Date 1154619041 -7200
# Node ID 9b406cb9d01058bf640b41f1e019998268106c3d
# Parent  27e4f43a0c3ebf8aa29bbb21296ee262143eaaef
added Isar/rule_insts.ML;

diff -r 27e4f43a0c3e -r 9b406cb9d010 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Thu Aug 03 17:30:40 2006 +0200
+++ b/src/Pure/IsaMakefile	Thu Aug 03 17:30:41 2006 +0200
@@ -39,8 +39,8 @@
   Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML		\
   Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML			\
   Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML			\
-  Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML		\
-  Isar/session.ML Isar/skip_proof.ML Isar/specification.ML			\
+  Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML 		\
+  Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML Isar/specification.ML	\
   Isar/term_style.ML Isar/thy_header.ML Isar/toplevel.ML			\
   ML-Systems/cpu-timer-basis.ML ML-Systems/cpu-timer-gc.ML			\
   ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML			\
diff -r 27e4f43a0c3e -r 9b406cb9d010 src/Pure/Isar/ROOT.ML
--- a/src/Pure/Isar/ROOT.ML	Thu Aug 03 17:30:40 2006 +0200
+++ b/src/Pure/Isar/ROOT.ML	Thu Aug 03 17:30:41 2006 +0200
@@ -61,6 +61,7 @@
 use "outer_syntax.ML";
 
 (*theory and proof operations*)
+use "rule_insts.ML";
 use "../simplifier.ML";
 use "find_theorems.ML";
 use "isar_thy.ML";