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/HOL/Tools/Metis/metis_reconstruct.ML
changeset 63170 eae6549dbea2
parent 61268 abe08fb15a12
child 63615 d786d54efc70 
--- a/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri May 27 20:13:06 2016 +0200
+++ b/src/HOL/Tools/Metis/metis_reconstruct.ML	Fri May 27 20:23:55 2016 +0200
@@ -192,7 +192,7 @@
       | _ =>
         let
           val thaa'bb' as [(tha', _), (thb', _)] =
-            map (`(Local_Defs.unfold ctxt meta_not_not)) [tha, thb]
+            map (`(Local_Defs.unfold0 ctxt meta_not_not)) [tha, thb]
         in
           if forall Thm.eq_thm_prop thaa'bb' then
             raise THM ("resolve_inc_tyvars: unique result expected", i, [tha, thb])
isabelle