src/Pure/tactic.ML

--- a/src/Pure/tactic.ML	Wed Aug 31 15:46:39 2005 +0200
+++ b/src/Pure/tactic.ML	Wed Aug 31 15:46:40 2005 +0200
@@ -693,7 +693,7 @@
 
     val raw_result = goal' RS Drule.rev_triv_goal;
     val prop' = prop_of raw_result;
-    val _ = conditional (not (Pattern.matches (Sign.tsig_of thy) (prop, prop'))) (fn () =>
+    val _ = conditional (not (Pattern.matches thy (prop, prop'))) (fn () =>
       err ("Proved a different theorem: " ^ Sign.string_of_term thy prop'));
   in
     Drule.conj_elim_precise (length props) raw_result