# HG changeset patch
# User wenzelm
# Date 1177353848 -7200
# Node ID 6f5068e26b8935d61f25d61bb5096ae3e08d983b
# Parent  d41fe3416f5217a37acb7ffdad321827492a3e33
simplified ProofContext.read_termTs;

diff -r d41fe3416f52 -r 6f5068e26b89 src/HOL/Tools/function_package/fundef_core.ML
--- a/src/HOL/Tools/function_package/fundef_core.ML	Mon Apr 23 18:38:42 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_core.ML	Mon Apr 23 20:44:08 2007 +0200
@@ -866,7 +866,7 @@
       val domT = domain_type fT
       val ranT = range_type fT
                             
-      val [default] = fst (Variable.importT_terms (fst (ProofContext.read_termTs lthy (K false) (K NONE) (K NONE) [] [(default_str, fT)])) lthy) (* FIXME *)
+      val default = singleton (ProofContext.read_termTs lthy) (default_str, fT)
 
       val congs = get_fundef_congs (Context.Proof lthy)
       val (globals, ctxt') = fix_globals domT ranT fvar lthy
diff -r d41fe3416f52 -r 6f5068e26b89 src/Pure/Tools/invoke.ML
--- a/src/Pure/Tools/invoke.ML	Mon Apr 23 18:38:42 2007 +0200
+++ b/src/Pure/Tools/invoke.ML	Mon Apr 23 20:44:08 2007 +0200
@@ -46,7 +46,9 @@
     val raw_insts' = zip_options params' raw_insts
       handle Library.UnequalLengths => error "Too many instantiations";
     val insts = map #1 raw_insts' ~~
-      prep_terms ctxt' (map (fn (t, u) => (u, Term.fastype_of t)) raw_insts');
+      Variable.polymorphic ctxt'
+        (prep_terms ctxt' (map (fn (t, u) => (u, Term.fastype_of t)) raw_insts'));
+
     val inst_rules =
       replicate (length types') Drule.termI @
       map (fn t =>
@@ -95,18 +97,15 @@
     |> Seq.hd
   end;
 
-(* FIXME *)
-fun read_terms ctxt args =
-  #1 (ProofContext.read_termTs ctxt (K false) (K NONE) (K NONE) [] args)
-  |> Variable.polymorphic ctxt;
-
-(* FIXME *)
-fun cert_terms ctxt args = map fst args;
+fun infer_terms ctxt =
+  ProofContext.infer_types ctxt o
+    (map (fn (t, T) => TypeInfer.constrain t (TypeInfer.paramify_vars T)));
 
 in
 
-fun invoke x = gen_invoke Attrib.attribute Locale.read_expr read_terms ProofContext.add_fixes x;
-fun invoke_i x = gen_invoke (K I) Locale.cert_expr cert_terms ProofContext.add_fixes_i x;
+fun invoke x =
+  gen_invoke Attrib.attribute Locale.read_expr ProofContext.read_termTs ProofContext.add_fixes x;
+fun invoke_i x = gen_invoke (K I) Locale.cert_expr infer_terms ProofContext.add_fixes_i x;
 
 end;