--- a/src/Pure/tactic.ML Sat May 15 21:09:54 2010 +0200
+++ b/src/Pure/tactic.ML Sat May 15 21:41:32 2010 +0200
@@ -156,7 +156,7 @@
fun dmatch_tac rls = ematch_tac (map make_elim rls);
(*Smash all flex-flex disagreement pairs in the proof state.*)
-val flexflex_tac = PRIMSEQ flexflex_rule;
+val flexflex_tac = PRIMSEQ Thm.flexflex_rule;
(*Remove duplicate subgoals.*)
val perm_tac = PRIMITIVE oo Thm.permute_prems;
@@ -185,7 +185,7 @@
(*Determine print names of goal parameters (reversed)*)
fun innermost_params i st =
- let val (_, _, Bi, _) = dest_state (st, i)
+ let val (_, _, Bi, _) = Thm.dest_state (st, i)
in Term.rename_wrt_term Bi (Logic.strip_params Bi) end;