--- a/src/Provers/typedsimp.ML Fri Oct 16 10:55:07 2009 +0200
+++ b/src/Provers/typedsimp.ML Sat Oct 17 00:52:37 2009 +0200
@@ -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 = standard (sym RSN (2,trans) RS sym);
+val split_eqn = Drule.standard (sym RSN (2,trans) RS sym);
(* [| a=b; b=c |] ==> reduce(a,c) *)
-val red_trans = standard (trans RS red_if_equal);
+val red_trans = Drule.standard (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) *)