1.1 --- a/src/Pure/Isar/attrib.ML	Thu Jul 27 23:28:25 2006 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Thu Jul 27 23:28:26 2006 +0200
     1.3 @@ -400,17 +400,22 @@
     1.4  fun params x = syntax (Args.and_list1 (Scan.lift (Scan.repeat Args.name)) >> RuleCases.params) x;
     1.5  
     1.6  
     1.7 -(* rule_format *)
     1.8 +(* rule format *)
     1.9  
    1.10  fun rule_format_att x = syntax (Args.mode "no_asm"
    1.11    >> (fn true => ObjectLogic.rule_format_no_asm | false => ObjectLogic.rule_format)) x;
    1.12  
    1.13 +fun elim_format x = no_args (Thm.rule_attribute (K Tactic.make_elim)) x;
    1.14 +
    1.15  
    1.16  (* misc rules *)
    1.17  
    1.18  fun standard x = no_args (Thm.rule_attribute (K Drule.standard)) x;
    1.19 -fun elim_format x = no_args (Thm.rule_attribute (K Tactic.make_elim)) x;
    1.20 -fun no_vars x = no_args (Thm.rule_attribute (K (#1 o Drule.freeze_thaw))) x;
    1.21 +
    1.22 +fun no_vars x = no_args (Thm.rule_attribute (fn ctxt => fn th =>
    1.23 +  let val ((_, [th']), _) = Variable.import true [th] (Context.proof_of ctxt)
    1.24 +  in th' end)) x;
    1.25 +
    1.26  fun eta_long x = no_args (Thm.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x;
    1.27  
    1.28