# HG changeset patch
# User wenzelm
# Date 1154035706 -7200
# Node ID a571d044891e10b9759552b421b2ada85f7966a5
# Parent  a7b027328d6e8e7595a461a3a2f55cafc459afc0
no_vars: based on Variable.import;
tuned;

diff -r a7b027328d6e -r a571d044891e src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Thu Jul 27 23:28:25 2006 +0200
+++ b/src/Pure/Isar/attrib.ML	Thu Jul 27 23:28:26 2006 +0200
@@ -400,17 +400,22 @@
 fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x;
 
 
-(* rule_format *)
+(* rule format *)
 
 fun rule_format_att x = syntax (Args.mode "no_asm"
   >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format)) x;
 
+fun elim_format x = no_args (Thm.rule_attribute (K Tactic.make_elim)) x;
+
 
 (* misc rules *)
 
 fun standard x = no_args (Thm.rule_attribute (K Drule.standard)) x;
-fun elim_format x = no_args (Thm.rule_attribute (K Tactic.make_elim)) x;
-fun no_vars x = no_args (Thm.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
+
+fun no_vars x = no_args (Thm.rule_attribute (fn ctxt => fn th =>
+  let val ((_, [th']), _) = Variable.import true [th] (Context.proof_of ctxt)
+  in th' end)) x;
+
 fun eta_long x = no_args (Thm.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x;