Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
proper argument type (amending 42fbb6abed5a);
authorwenzelm
Fri, 26 Jul 2019 15:21:02 +0200
changeset 70418 d23cfb85438a
parent 70417 eb6ff14767cd
child 70419 ea5a492cd196
proper argument type (amending 42fbb6abed5a);
src/Pure/Proof/proof_syntax.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Proof/proof_syntax.ML	Fri Jul 26 14:43:56 2019 +0200
+++ b/src/Pure/Proof/proof_syntax.ML	Fri Jul 26 15:21:02 2019 +0200
@@ -129,7 +129,7 @@
             Proofterm.incr_pboundvars 0 (~1) (prf_of [] prf))
       | prf_of [] (Const ("Pure.AppP", _) $ prf1 $ prf2) =
           prf_of [] prf1 %% prf_of [] prf2
-      | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type (_, [T]))) =
+      | prf_of Ts (Const ("Pure.Appt", _) $ prf $ Const ("Pure.type", Type ("itself", [T]))) =
           prf_of (T::Ts) prf
       | prf_of [] (Const ("Pure.Appt", _) $ prf $ t) = prf_of [] prf %
           (case t of Const ("Pure.dummy_pattern", _) => NONE | _ => SOME (mk_term t))
isabelle