src/Provers/typedsimp.ML
changeset 35021 c839a4c670c6
parent 33339 d41f77196338
child 45659 09539cdffcd7
--- a/src/Provers/typedsimp.ML	Sun Feb 07 19:31:55 2010 +0100
+++ b/src/Provers/typedsimp.ML	Sun Feb 07 19:33:34 2010 +0100
@@ -43,11 +43,11 @@
 (*For simplifying both sides of an equation:
       [| a=c; b=c |] ==> b=a
   Can use resolve_tac [split_eqn] to prepare an equation for simplification. *)
-val split_eqn = Drule.standard (sym RSN (2,trans) RS sym);
+val split_eqn = Drule.export_without_context (sym RSN (2,trans) RS sym);
 
 
 (*    [| a=b; b=c |] ==> reduce(a,c)  *)
-val red_trans = Drule.standard (trans RS red_if_equal);
+val red_trans = Drule.export_without_context (trans RS red_if_equal);
 
 (*For REWRITE rule: Make a reduction rule for simplification, e.g.
   [| a: C(0); ... ; a=c: C(0) |] ==> rec(0,a,b) = c: C(0) *)