Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/goals.ML
changeset 17203 29b2563f5c11
parent 16787 b6b6e2faaa41
child 17224 a78339014063 
--- a/src/Pure/goals.ML	Wed Aug 31 15:46:39 2005 +0200
+++ b/src/Pure/goals.ML	Wed Aug 31 15:46:40 2005 +0200
@@ -752,7 +752,7 @@
                     (map (Sign.string_of_term thy)
                      (List.filter (fn x => (not (in_locale [x] thy)))
                       hyps)))
-            else if Pattern.matches (Sign.tsig_of thy)
+            else if Pattern.matches thy
                                     (Envir.beta_norm (term_of chorn), Envir.beta_norm prop)
                  then final_th
             else  !result_error_fn state "proved a different theorem"
isabelle