# HG changeset patch # User wenzelm # Date 1138465735 -3600 # Node ID 213b7341abb6418dd01589e1220ef697b5cb25e5 # Parent 24dcd5b0e26b3247794792b7c5bc34551bf65271 (un)folded: support object-level rewrites; diff -r 24dcd5b0e26b -r 213b7341abb6 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sat Jan 28 17:28:54 2006 +0100 +++ b/src/Pure/Isar/attrib.ML Sat Jan 28 17:28:55 2006 +0100 @@ -396,8 +396,8 @@ (* unfold / fold definitions *) -val unfolded = syntax (thmss >> (fn defs => Thm.rule_attribute (K (Tactic.rewrite_rule defs)))); -val folded = syntax (thmss >> (fn defs => Thm.rule_attribute (K (Tactic.fold_rule defs)))); +val unfolded = syntax (thmss >> (fn defs => Thm.rule_attribute (K (ObjectLogic.unfold defs)))); +val folded = syntax (thmss >> (fn defs => Thm.rule_attribute (K (ObjectLogic.fold defs)))); (* rule cases *)