# HG changeset patch
# User wenzelm
# Date 1188595040 -7200
# Node ID 2439587f516bc7d2ee766adc496a015eab2938eb
# Parent  8d5326f0098b4e642ae36708cc79ea18665c9a44
legacy_infer_term: ProofContext.mode_schematic;

diff -r 8d5326f0098b -r 2439587f516b src/HOLCF/Tools/domain/domain_theorems.ML
--- a/src/HOLCF/Tools/domain/domain_theorems.ML	Fri Aug 31 18:46:37 2007 +0200
+++ b/src/HOLCF/Tools/domain/domain_theorems.ML	Fri Aug 31 23:17:20 2007 +0200
@@ -54,9 +54,13 @@
 
 (* ----- general proof facilities ------------------------------------------- *)
 
+fun legacy_infer_term thy t =
+  let val ctxt = ProofContext.set_mode ProofContext.mode_schematic (ProofContext.init thy)
+  in singleton (Syntax.check_terms ctxt) (Sign.intern_term thy t) end;
+
 fun pg'' thy defs t tacs =
   let
-    val t' = FixrecPackage.legacy_infer_term thy t;
+    val t' = legacy_infer_term thy t;
     val asms = Logic.strip_imp_prems t';
     val prop = Logic.strip_imp_concl t';
     fun tac prems =