# HG changeset patch
# User blanchet
# Date 1272372910 -7200
# Node ID 71cc00ea576868d78a91bd15c2a9c45b73d13515
# Parent  a04cf47046689100d3ef50cec4dc0aab13b626df
allow schematic variables in types in terms that are reconstructed by Sledgehammer

diff -r a04cf4704668 -r 71cc00ea5768 src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
--- 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;