--- a/TFL/tfl.ML Sun Apr 15 14:31:47 2007 +0200
+++ b/TFL/tfl.ML Sun Apr 15 14:31:49 2007 +0200
@@ -367,9 +367,8 @@
(*For Isabelle, the lhs of a definition must be a constant.*)
fun mk_const_def sign (c, Ty, rhs) =
- Sign.infer_types (Sign.pp sign) sign (Sign.consts_of sign) (K NONE) (K NONE) Name.context false
- ([Const("==",dummyT) $ Const(c,Ty) $ rhs], propT)
- |> #1;
+ #1 (singleton (ProofContext.infer_types (ProofContext.init sign))
+ (Const("==",dummyT) $ Const(Sign.full_name sign c,Ty) $ rhs, propT));
(*Make all TVars available for instantiation by adding a ? to the front*)
fun poly_tvars (Type(a,Ts)) = Type(a, map (poly_tvars) Ts)
--- a/src/HOL/Nominal/nominal_primrec.ML Sun Apr 15 14:31:47 2007 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML Sun Apr 15 14:31:49 2007 +0200
@@ -206,10 +206,11 @@
val frees = ls @ x :: rs;
val rhs = list_abs_free (frees,
list_comb (Const (rec_name, dummyT), fs @ [Free x]))
- val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def",
- Logic.mk_equals (Const (fname, dummyT), rhs));
- val defpair' as (_, _ $ _ $ t) = Theory.inferT_axm thy defpair
- in (defpair', subst_bounds (rev (map Free frees), strip_abs_body t)) end;
+ val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
+ val def_prop as _ $ _ $ t =
+ singleton (ProofContext.infer_types (ProofContext.init thy))
+ (Logic.mk_equals (Const (fname, dummyT), rhs), propT) |> #1;
+ in ((def_name, def_prop), subst_bounds (rev (map Free frees), strip_abs_body t)) end;
(* find datatypes which contain all datatypes in tnames' *)
--- a/src/HOL/Tools/primrec_package.ML Sun Apr 15 14:31:47 2007 +0200
+++ b/src/HOL/Tools/primrec_package.ML Sun Apr 15 14:31:49 2007 +0200
@@ -16,6 +16,7 @@
-> theory -> thm list * theory
val add_primrec_unchecked_i: string -> ((bstring * term) * attribute list) list
-> theory -> thm list * theory
+ (* FIXME !? *)
val gen_primrec: ((bstring * attribute list) * thm list -> theory -> (bstring * thm list) * theory)
-> ((bstring * attribute list) * term -> theory -> (bstring * thm) * theory)
-> string -> ((bstring * attribute list) * term) list
@@ -42,16 +43,16 @@
(* preprocessing of equations *)
-fun process_eqn thy eq rec_fns =
+fun process_eqn thy eq rec_fns =
let
- val (lhs, rhs) =
+ val (lhs, rhs) =
if null (term_vars eq) then
HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
handle TERM _ => raise RecError "not a proper equation"
else raise RecError "illegal schematic variable(s)";
val (recfun, args) = strip_comb lhs;
- val fnameT = dest_Const recfun handle TERM _ =>
+ val fnameT = dest_Const recfun handle TERM _ =>
raise RecError "function is not declared as constant in theory";
val (ls', rest) = take_prefix is_Free args;
@@ -73,7 +74,7 @@
fun check_vars _ [] = ()
| check_vars s vars = raise RecError (s ^ commas_quote (map fst vars))
in
- if length middle > 1 then
+ if length middle > 1 then
raise RecError "more than one non-variable in pattern"
else
(check_vars "repeated variable names in pattern: " (duplicates (op =) lfrees);
@@ -147,14 +148,14 @@
let
val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map fst recs;
- val subs = map (rpair dummyT o fst)
+ val subs = map (rpair dummyT o fst)
(rev (rename_wrt_term rhs rargs));
- val (rhs', (fnameTs'', fnss'')) =
+ val (rhs', (fnameTs'', fnss'')) =
(subst (map (fn ((x, y), z) =>
(Free x, (body_index y, Free z)))
(recs ~~ subs)) rhs (fnameTs', fnss'))
handle RecError s => primrec_eq_err thy s eq
- in (fnameTs'', fnss'',
+ in (fnameTs'', fnss'',
(list_abs_free (cargs' @ subs @ ls @ rs, rhs'))::fns)
end)
@@ -166,7 +167,7 @@
let
val (_, _, eqns) = the (AList.lookup (op =) rec_eqns fnameT);
val (fnameTs', fnss', fns) = fold_rev (trans eqns) constrs
- ((i, fnameT)::fnameTs, fnss, [])
+ ((i, fnameT)::fnameTs, fnss, [])
in
(fnameTs', (i, (fname, #1 (snd (hd eqns)), fns))::fnss')
end
@@ -200,9 +201,11 @@
((map snd ls) @ [dummyT])
(list_comb (Const (rec_name, dummyT),
fs @ map Bound (0 ::(length ls downto 1))))
- val defpair = (Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def",
- Logic.mk_equals (Const (fname, dummyT), rhs))
- in Theory.inferT_axm thy defpair end;
+ val def_name = Sign.base_name fname ^ "_" ^ Sign.base_name tname ^ "_def";
+ val def_prop =
+ singleton (ProofContext.infer_types (ProofContext.init thy))
+ (Logic.mk_equals (Const (fname, dummyT), rhs), propT) |> #1;
+ in (def_name, def_prop) end;
(* find datatypes which contain all datatypes in tnames' *)
@@ -236,12 +239,12 @@
val rec_eqns = fold_rev (process_eqn thy o snd) eqns [] ;
val tnames = distinct (op =) (map (#1 o snd) rec_eqns);
val dts = find_dts dt_info tnames tnames;
- val main_fns =
+ val main_fns =
map (fn (tname, {index, ...}) =>
- (index,
+ (index,
(fst o the o find_first (fn f => (#1 o snd) f = tname)) rec_eqns))
dts;
- val {descr, rec_names, rec_rewrites, ...} =
+ val {descr, rec_names, rec_rewrites, ...} =
if null dts then
primrec_err ("datatypes " ^ commas_quote tnames ^ "\nare not mutually recursive")
else snd (hd dts);
@@ -308,7 +311,7 @@
fun gen_primrec note def alt_name specs =
gen_primrec_i note def alt_name (map (fn ((name, t), atts) => ((name, atts), t)) specs);
-end; (*local*)
+end;
(* outer syntax *)
@@ -334,6 +337,4 @@
end;
-
end;
-
--- a/src/HOL/Tools/res_reconstruct.ML Sun Apr 15 14:31:47 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Sun Apr 15 14:31:49 2007 +0200
@@ -282,12 +282,7 @@
vt0 holds the initial sort constraints, from the conjecture clauses.*)
fun clause_of_strees_aux ctxt vt0 ts =
let val (vt, dt) = lits_of_strees ctxt (vt0,[]) ts
- val infer = Sign.infer_types (ProofContext.pp ctxt) (ProofContext.theory_of ctxt)
- (ProofContext.consts_of ctxt) (Variable.def_type ctxt false)
- (Variable.def_sort ctxt) (Variable.names_of ctxt) true
- in
- #1(infer ([fix_sorts vt dt], HOLogic.boolT))
- end;
+ in #1 (singleton (ProofContext.infer_types ctxt) (fix_sorts vt dt, HOLogic.boolT)) end;
(*Quantification over a list of Vars. FUXNE: for term.ML??*)
fun list_all_var ([], t: term) = t
--- a/src/Pure/Isar/rule_insts.ML Sun Apr 15 14:31:47 2007 +0200
+++ b/src/Pure/Isar/rule_insts.ML Sun Apr 15 14:31:49 2007 +0200
@@ -131,8 +131,8 @@
let
val ctxt' = ctxt |> Variable.declare_thm thm
|> fold (fn a => Variable.declare_internal (Logic.mk_type (TFree (a, [])))) (Drule.add_used thm []); (* FIXME tmp *)
- val tvars = Drule.fold_terms Term.add_tvars thm [];
- val vars = Drule.fold_terms Term.add_vars thm [];
+ val tvars = Thm.fold_terms Term.add_tvars thm [];
+ val vars = Thm.fold_terms Term.add_vars thm [];
val ((type_insts, term_insts), insts) = read_insts ctxt' (map snd mixed_insts) (tvars, vars);
val _ = (*assign internalized values*)
--- a/src/Pure/Isar/theory_target.ML Sun Apr 15 14:31:47 2007 +0200
+++ b/src/Pure/Isar/theory_target.ML Sun Apr 15 14:31:49 2007 +0200
@@ -213,8 +213,8 @@
val nprems = Thm.nprems_of th' - Thm.nprems_of th;
(*export fixes*)
- val tfrees = map TFree (Drule.fold_terms Term.add_tfrees th' []);
- val frees = map Free (Drule.fold_terms Term.add_frees th' []);
+ val tfrees = map TFree (Thm.fold_terms Term.add_tfrees th' []);
+ val frees = map Free (Thm.fold_terms Term.add_frees th' []);
val (th'' :: vs) = (th' :: map (Drule.mk_term o cert) (map Logic.mk_type tfrees @ frees))
|> Variable.export ctxt thy_ctxt
|> Drule.zero_var_indexes_list;
--- a/src/Pure/Tools/nbe.ML Sun Apr 15 14:31:47 2007 +0200
+++ b/src/Pure/Tools/nbe.ML Sun Apr 15 14:31:49 2007 +0200
@@ -148,8 +148,8 @@
error ("Illegal schematic type variables in normalized term: "
^ setmp show_types true (Sign.string_of_term thy) t);
val ty = type_of t;
- fun constrain t = Sign.infer_types (Sign.pp thy) thy (Sign.consts_of thy)
- (K NONE) (K NONE) Name.context false ([t], ty) |> fst;
+ fun constrain t = (* FIXME really pat? *)
+ #1 (singleton (ProofContext.infer_types_pat (ProofContext.init thy)) (t, ty));
val _ = ensure_funs thy funcgr t;
in
t