--- 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
--- 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;