src/Provers/hypsubst.ML
changeset 32957 675c0c7e6a37
parent 30515 bca05b17b618
child 35021 c839a4c670c6
--- a/src/Provers/hypsubst.ML	Fri Oct 16 10:55:07 2009 +0200
+++ b/src/Provers/hypsubst.ML	Sat Oct 17 00:52:37 2009 +0200
@@ -165,7 +165,7 @@
 
 end;
 
-val ssubst = standard (Data.sym RS Data.subst);
+val ssubst = Drule.standard (Data.sym RS Data.subst);
 
 fun inst_subst_tac b rl = CSUBGOAL (fn (cBi, i) =>
   case try (Logic.strip_assums_hyp #> hd #>