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.
allow schematic variables in types in terms that are reconstructed by Sledgehammer
authorblanchet
Tue, 27 Apr 2010 14:55:10 +0200
changeset 36477 71cc00ea5768
parent 36476 a04cf4704668
child 36478 1aba777a367f
allow schematic variables in types in terms that are reconstructed by Sledgehammer
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 14:27:47 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML	Tue Apr 27 14:55:10 2010 +0200
@@ -326,7 +326,8 @@
 fun clause_of_strees ctxt vt ts =
   let val (vt, dt) = lits_of_strees (ProofContext.theory_of ctxt) (vt, []) ts in
     dt |> repair_sorts vt |> TypeInfer.constrain HOLogic.boolT
-       |> Syntax.check_term ctxt
+       |> Syntax.check_term (ProofContext.set_mode ProofContext.mode_schematic
+                                                   ctxt)
   end
 
 fun gen_all_vars t = fold_rev Logic.all (OldTerm.term_vars t) t;
isabelle