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.
ProofContext.inferred_param;
authorwenzelm
Tue, 24 Jan 2006 00:43:32 +0100
changeset 18769 e90eb0bc0ddd
parent 18768 6e97b57cdcba
child 18770 434f660d3068
ProofContext.inferred_param;
src/Pure/Isar/obtain.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/obtain.ML	Tue Jan 24 00:43:31 2006 +0100
+++ b/src/Pure/Isar/obtain.ML	Tue Jan 24 00:43:32 2006 +0100
@@ -199,7 +199,7 @@
   in (xs' @ ys', rule') end;
 
 fun inferred_type (x, _, mx) ctxt =
-  let val ((_, T), ctxt') = ProofContext.inferred_type x ctxt
+  let val ((_, T), ctxt') = ProofContext.inferred_param x ctxt
   in ((x, SOME T, mx), ctxt') end;
 
 fun gen_guess prep_vars raw_vars int state =
isabelle