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/Proof/proof_checker.ML
changeset 70493 a9053fa30909
parent 70447 755d58b48cec
child 70838 e381e2624077 
--- a/src/Pure/Proof/proof_checker.ML	Fri Aug 09 10:30:54 2019 +0200
+++ b/src/Pure/Proof/proof_checker.ML	Fri Aug 09 15:58:26 2019 +0200
@@ -84,7 +84,7 @@
             Thm.instantiate (ctye, []) (forall_intr_vars (Thm.forall_intr_frees thm'))
           end;
 
-        fun thm_of _ _ (PThm (_, ((name, prop', SOME Ts, _), _))) =
+        fun thm_of _ _ (PThm ({name, prop = prop', types = SOME Ts, ...}, _)) =
               let
                 val thm = Thm.unconstrainT (Drule.implies_intr_hyps (lookup name));
                 val prop = Thm.prop_of thm;
isabelle