src/Pure/Isar/attrib.ML
changeset 35624 c4e29a0bb8c1
parent 35021 c839a4c670c6
child 35625 9c818cab0dd0
--- a/src/Pure/Isar/attrib.ML	Sat Mar 06 19:17:59 2010 +0000
+++ b/src/Pure/Isar/attrib.ML	Sun Mar 07 11:57:16 2010 +0100
@@ -245,8 +245,8 @@
 fun unfolded_syntax rule =
   thms >> (fn ths => Thm.rule_attribute (fn context => rule (Context.proof_of context) ths));
 
-val unfolded = unfolded_syntax LocalDefs.unfold;
-val folded = unfolded_syntax LocalDefs.fold;
+val unfolded = unfolded_syntax Local_Defs.unfold;
+val folded = unfolded_syntax Local_Defs.fold;
 
 
 (* rule format *)
@@ -311,7 +311,7 @@
   setup (Binding.name "rulify") (Scan.succeed ObjectLogic.declare_rulify)
     "declaration of rulify rule" #>
   setup (Binding.name "rotated") (Scan.lift rotated) "rotated theorem premises" #>
-  setup (Binding.name "defn") (add_del LocalDefs.defn_add LocalDefs.defn_del)
+  setup (Binding.name "defn") (add_del Local_Defs.defn_add Local_Defs.defn_del)
     "declaration of definitional transformations" #>
   setup (Binding.name "abs_def") (Scan.succeed (Thm.rule_attribute (K Drule.abs_def)))
     "abstract over free variables of a definition"));