--- a/src/FOL/FOL.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/FOL.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/FOL.thy
- ID: $Id$
Author: Lawrence C Paulson and Markus Wenzel
*)
--- a/src/FOL/ROOT.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ROOT.ML Fri Jul 10 00:10:36 2009 +0200
@@ -1,7 +1,3 @@
-(* Title: FOL/ROOT.ML
- ID: $Id$
-
-First-Order Logic with Natural Deduction.
-*)
+(* First-Order Logic with Natural Deduction *)
use_thy "FOL";
--- a/src/FOL/cladata.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/cladata.ML Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/cladata.ML
- ID: $Id$
Author: Tobias Nipkow
Copyright 1996 University of Cambridge
--- a/src/FOL/ex/Classical.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Classical.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
-(* Title: FOL/ex/Classical
- ID: $Id$
+(* Title: FOL/ex/Classical.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
*)
--- a/src/FOL/ex/First_Order_Logic.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/First_Order_Logic.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/First_Order_Logic.thy
- ID: $Id$
Author: Markus Wenzel, TU Munich
*)
--- a/src/FOL/ex/Foundation.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Foundation.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
-(* Title: FOL/ex/Foundation.ML
- ID: $Id$
+(* Title: FOL/ex/Foundation.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/If.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/If.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/If.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Intro.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Intro.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Intro.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/FOL/ex/Intuitionistic.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Intuitionistic.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,12 +1,13 @@
-(* Title: FOL/ex/Intuitionistic
- ID: $Id$
+(* Title: FOL/ex/Intuitionistic.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
-header{*Intuitionistic First-Order Logic*}
+header {* Intuitionistic First-Order Logic *}
-theory Intuitionistic imports IFOL begin
+theory Intuitionistic
+imports IFOL
+begin
(*
Single-step ML commands:
@@ -422,4 +423,3 @@
end
-
--- a/src/FOL/ex/Miniscope.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Miniscope.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Miniscope.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
--- a/src/FOL/ex/Nat.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Nat.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Nat.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/FOL/ex/Natural_Numbers.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Natural_Numbers.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,11 +1,12 @@
(* Title: FOL/ex/Natural_Numbers.thy
- ID: $Id$
Author: Markus Wenzel, TU Munich
*)
header {* Natural numbers *}
-theory Natural_Numbers imports FOL begin
+theory Natural_Numbers
+imports FOL
+begin
text {*
Theory of the natural numbers: Peano's axioms, primitive recursion.
--- a/src/FOL/ex/Prolog.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Prolog.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
-(* Title: FOL/ex/prolog.thy
- ID: $Id$
+(* Title: FOL/ex/Prolog.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/FOL/ex/Propositional_Cla.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Propositional_Cla.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Propositional_Cla.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Propositional_Int.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Propositional_Int.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Propositional_Int.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Quantifiers_Cla.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Quantifiers_Cla.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Quantifiers_Int.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Quantifiers_Int.thy Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/ex/Quantifiers_Int.thy Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/ex/Quantifiers_Int.thy
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/fologic.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/fologic.ML Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/fologic.ML
- ID: $Id$
Author: Lawrence C Paulson
Abstract syntax operations for FOL.
--- a/src/FOL/intprover.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/intprover.ML Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
-(* Title: FOL/int-prover
- ID: $Id$
+(* Title: FOL/intprover.ML
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
--- a/src/FOL/simpdata.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/FOL/simpdata.ML Fri Jul 10 00:10:36 2009 +0200
@@ -1,5 +1,4 @@
(* Title: FOL/simpdata.ML
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1994 University of Cambridge
--- a/src/HOL/Library/Library/ROOT.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/HOL/Library/Library/ROOT.ML Fri Jul 10 00:10:36 2009 +0200
@@ -1,3 +1,1 @@
-(* $Id$ *)
-
use_thys ["Library", "List_Prefix", "List_lexord", "Sublist_Order"];
--- a/src/HOL/Library/Library/document/root.tex Thu Jul 09 23:05:59 2009 +0200
+++ b/src/HOL/Library/Library/document/root.tex Fri Jul 10 00:10:36 2009 +0200
@@ -1,6 +1,3 @@
-
-% $Id$
-
\documentclass[11pt,a4paper]{article}
\usepackage{ifthen}
\usepackage[latin1]{inputenc}
--- a/src/HOL/Library/README.html Thu Jul 09 23:05:59 2009 +0200
+++ b/src/HOL/Library/README.html Fri Jul 10 00:10:36 2009 +0200
@@ -1,7 +1,5 @@
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-<!-- $Id$ -->
-
<html>
<head>
--- a/src/Pure/Isar/expression.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/Isar/expression.ML Fri Jul 10 00:10:36 2009 +0200
@@ -492,7 +492,7 @@
val export = Variable.export_morphism goal_ctxt context;
val exp_fact = Drule.zero_var_indexes_list o map Thm.strip_shyps o Morphism.fact export;
- val exp_term = TermSubst.zero_var_indexes o Morphism.term export;
+ val exp_term = Term_Subst.zero_var_indexes o Morphism.term export;
val exp_typ = Logic.type_map exp_term;
val export' = Morphism.morphism {binding = I, typ = exp_typ, term = exp_term, fact = exp_fact};
in ((propss, deps, export'), goal_ctxt) end;
--- a/src/Pure/Isar/rule_insts.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/Isar/rule_insts.ML Fri Jul 10 00:10:36 2009 +0200
@@ -58,7 +58,7 @@
end;
fun instantiate inst =
- TermSubst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
+ Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #>
Envir.beta_norm;
fun make_instT f v =
@@ -124,7 +124,7 @@
end;
val type_insts1 = map readT type_insts;
- val instT1 = TermSubst.instantiateT type_insts1;
+ val instT1 = Term_Subst.instantiateT type_insts1;
val vars1 = map (apsnd instT1) vars;
--- a/src/Pure/Isar/theory_target.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/Isar/theory_target.ML Fri Jul 10 00:10:36 2009 +0200
@@ -130,7 +130,7 @@
val instT = map_filter (fn (TVar v, T) => SOME (v, T) | _ => NONE) (tvars ~~ tfrees);
val inst = filter (is_Var o fst) (vars ~~ frees);
val cinstT = map (pairself certT o apfst TVar) instT;
- val cinst = map (pairself (cert o Term.map_types (TermSubst.instantiateT instT))) inst;
+ val cinst = map (pairself (cert o Term.map_types (Term_Subst.instantiateT instT))) inst;
val result' = Thm.instantiate (cinstT, cinst) result;
(*import assumes/defines*)
--- a/src/Pure/consts.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/consts.ML Fri Jul 10 00:10:36 2009 +0200
@@ -215,7 +215,7 @@
val vars = map Term.dest_TVar (typargs consts (c, declT));
val inst = vars ~~ Ts handle UnequalLengths =>
raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]);
- in declT |> TermSubst.instantiateT inst end;
+ in declT |> Term_Subst.instantiateT inst end;
--- a/src/Pure/drule.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/drule.ML Fri Jul 10 00:10:36 2009 +0200
@@ -278,7 +278,7 @@
let
val thy = Theory.merge_list (map Thm.theory_of_thm ths);
val certT = Thm.ctyp_of thy and cert = Thm.cterm_of thy;
- val (instT, inst) = TermSubst.zero_var_indexes_inst (map Thm.full_prop_of ths);
+ val (instT, inst) = Term_Subst.zero_var_indexes_inst (map Thm.full_prop_of ths);
val cinstT = map (fn (v, T) => (certT (TVar v), certT T)) instT;
val cinst = map (fn (v, t) => (cert (Var v), cert t)) inst;
in map (Thm.adjust_maxidx_thm ~1 o Thm.instantiate (cinstT, cinst)) ths end;
--- a/src/Pure/more_thm.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/more_thm.ML Fri Jul 10 00:10:36 2009 +0200
@@ -274,7 +274,7 @@
val instT0 = rev (Term.add_tvars prop []) |> map (fn v as ((a, _), S) => (v, TFree (a, S)));
val instT = map (fn (v, T) => (certT (TVar v), certT T)) instT0;
val inst = rev (Term.add_vars prop []) |> map (fn ((a, i), T) =>
- let val T' = TermSubst.instantiateT instT0 T
+ let val T' = Term_Subst.instantiateT instT0 T
in (cert (Var ((a, i), T')), cert (Free ((a, T')))) end);
in Thm.instantiate (instT, inst) th end;
--- a/src/Pure/proofterm.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/proofterm.ML Fri Jul 10 00:10:36 2009 +0200
@@ -441,12 +441,12 @@
(**** substitutions ****)
-fun del_conflicting_tvars envT T = TermSubst.instantiateT
+fun del_conflicting_tvars envT T = Term_Subst.instantiateT
(map_filter (fn ixnS as (_, S) =>
(Type.lookup envT ixnS; NONE) handle TYPE _ =>
SOME (ixnS, TFree ("'dummy", S))) (OldTerm.typ_tvars T)) T;
-fun del_conflicting_vars env t = TermSubst.instantiate
+fun del_conflicting_vars env t = Term_Subst.instantiate
(map_filter (fn ixnS as (_, S) =>
(Type.lookup (type_env env) ixnS; NONE) handle TYPE _ =>
SOME (ixnS, TFree ("'dummy", S))) (OldTerm.term_tvars t),
@@ -689,16 +689,16 @@
fun generalize (tfrees, frees) idx =
map_proof_terms_option
- (TermSubst.generalize_option (tfrees, frees) idx)
- (TermSubst.generalizeT_option tfrees idx);
+ (Term_Subst.generalize_option (tfrees, frees) idx)
+ (Term_Subst.generalizeT_option tfrees idx);
(***** instantiation *****)
fun instantiate (instT, inst) =
map_proof_terms_option
- (TermSubst.instantiate_option (instT, map (apsnd remove_types) inst))
- (TermSubst.instantiateT_option instT);
+ (Term_Subst.instantiate_option (instT, map (apsnd remove_types) inst))
+ (Term_Subst.instantiateT_option instT);
(***** lifting *****)
--- a/src/Pure/term_ord.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/term_ord.ML Fri Jul 10 00:10:36 2009 +0200
@@ -205,5 +205,6 @@
end;
structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord);
+structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord);
structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord);
structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord);
--- a/src/Pure/term_subst.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/term_subst.ML Fri Jul 10 00:10:36 2009 +0200
@@ -1,11 +1,15 @@
(* Title: Pure/term_subst.ML
Author: Makarius
-Efficient term substitution -- avoids copying.
+Efficient type/term substitution -- avoids copying.
*)
signature TERM_SUBST =
sig
+ val map_atypsT_option: (typ -> typ option) -> typ -> typ option
+ val map_atyps_option: (typ -> typ option) -> term -> term option
+ val map_types_option: (typ -> typ option) -> term -> term option
+ val map_aterms_option: (term -> term option) -> term -> term option
val generalize: string list * string list -> int -> term -> term
val generalizeT: string list -> int -> typ -> typ
val generalize_option: string list * string list -> int -> term -> term option
@@ -25,15 +29,67 @@
((indexname * sort) * typ) list * ((indexname * typ) * term) list
end;
-structure TermSubst: TERM_SUBST =
+structure Term_Subst: TERM_SUBST =
struct
+(* indication of same result *)
+
+exception SAME;
+
+fun same_fn f x =
+ (case f x of
+ NONE => raise SAME
+ | SOME y => y);
+
+fun option_fn f x =
+ SOME (f x) handle SAME => NONE;
+
+
+(* generic mapping *)
+
+local
+
+fun map_atypsT_same f =
+ let
+ fun typ (Type (a, Ts)) = Type (a, typs Ts)
+ | typ T = f T
+ and typs (T :: Ts) = (typ T :: (typs Ts handle SAME => Ts) handle SAME => T :: typs Ts)
+ | typs [] = raise SAME;
+ in typ end;
+
+fun map_types_same f =
+ let
+ fun term (Const (a, T)) = Const (a, f T)
+ | term (Free (a, T)) = Free (a, f T)
+ | term (Var (v, T)) = Var (v, f T)
+ | term (Bound _) = raise SAME
+ | term (Abs (x, T, t)) =
+ (Abs (x, f T, term t handle SAME => t)
+ handle SAME => Abs (x, T, term t))
+ | term (t $ u) = (term t $ (term u handle SAME => u) handle SAME => t $ term u);
+ in term end;
+
+fun map_aterms_same f =
+ let
+ fun term (Abs (x, T, t)) = Abs (x, T, term t)
+ | term (t $ u) = (term t $ (term u handle SAME => u) handle SAME => t $ term u)
+ | term a = f a;
+ in term end;
+
+in
+
+val map_atypsT_option = option_fn o map_atypsT_same o same_fn;
+val map_atyps_option = option_fn o map_types_same o map_atypsT_same o same_fn;
+val map_types_option = option_fn o map_types_same o same_fn;
+val map_aterms_option = option_fn o map_aterms_same o same_fn;
+
+end;
+
+
(* generalization of fixed variables *)
local
-exception SAME;
-
fun generalizeT_same [] _ _ = raise SAME
| generalizeT_same tfrees idx ty =
let
@@ -84,8 +140,6 @@
fun no_indexes1 inst = map no_index inst;
fun no_indexes2 (inst1, inst2) = (map no_index inst1, map no_index inst2);
-exception SAME;
-
fun instantiateT_same maxidx instT ty =
let
fun maxify i = if i > ! maxidx then maxidx := i else ();
--- a/src/Pure/thm.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/thm.ML Fri Jul 10 00:10:36 2009 +0200
@@ -995,7 +995,7 @@
val _ = exists bad_term hyps andalso
raise THM ("generalize: variable free in assumptions", 0, [th]);
- val gen = TermSubst.generalize (tfrees, frees) idx;
+ val gen = Term_Subst.generalize (tfrees, frees) idx;
val prop' = gen prop;
val tpairs' = map (pairself gen) tpairs;
val maxidx' = maxidx_tpairs tpairs' (maxidx_of_term prop');
@@ -1066,7 +1066,7 @@
val Thm (der, {thy_ref, hyps, shyps, tpairs, prop, ...}) = th;
val (inst', (instT', (thy_ref', shyps'))) =
(thy_ref, shyps) |> fold_map add_inst inst ||> fold_map add_instT instT;
- val subst = TermSubst.instantiate_maxidx (instT', inst');
+ val subst = Term_Subst.instantiate_maxidx (instT', inst');
val (prop', maxidx1) = subst prop ~1;
val (tpairs', maxidx') =
fold_map (fn (t, u) => fn i => subst t i ||>> subst u) tpairs maxidx1;
@@ -1088,8 +1088,8 @@
val Cterm {thy_ref, t, T, sorts, ...} = ct;
val (inst', (instT', (thy_ref', sorts'))) =
(thy_ref, sorts) |> fold_map add_inst inst ||> fold_map add_instT instT;
- val subst = TermSubst.instantiate_maxidx (instT', inst');
- val substT = TermSubst.instantiateT_maxidx instT';
+ val subst = Term_Subst.instantiate_maxidx (instT', inst');
+ val substT = Term_Subst.instantiateT_maxidx instT';
val (t', maxidx1) = subst t ~1;
val (T', maxidx') = substT T maxidx1;
in Cterm {thy_ref = thy_ref', t = t', T = T', sorts = sorts', maxidx = maxidx'} end
--- a/src/Pure/type_infer.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/type_infer.ML Fri Jul 10 00:10:36 2009 +0200
@@ -64,7 +64,7 @@
else (inst, used);
val name_context' = (fold o fold_types) Term.declare_typ_names ts name_context;
val (inst, _) = fold_rev subst_param (fold Term.add_tvars ts []) ([], name_context');
- in (map o map_types) (TermSubst.instantiateT inst) ts end;
+ in (map o map_types) (Term_Subst.instantiateT inst) ts end;
--- a/src/Pure/variable.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Pure/variable.ML Fri Jul 10 00:10:36 2009 +0200
@@ -360,14 +360,14 @@
fun exportT_terms inner outer =
let val mk_tfrees = exportT_inst inner outer in
fn ts => ts |> map
- (TermSubst.generalize (mk_tfrees ts, [])
+ (Term_Subst.generalize (mk_tfrees ts, [])
(fold (Term.fold_types Term.maxidx_typ) ts ~1 + 1))
end;
fun export_terms inner outer =
let val (mk_tfrees, tfrees) = export_inst inner outer in
fn ts => ts |> map
- (TermSubst.generalize (mk_tfrees ts, tfrees)
+ (Term_Subst.generalize (mk_tfrees ts, tfrees)
(fold Term.maxidx_term ts ~1 + 1))
end;
@@ -376,8 +376,8 @@
val (mk_tfrees, frees) = export_inst (declare_prf prf inner) outer;
val tfrees = mk_tfrees [];
val idx = Proofterm.maxidx_proof prf ~1 + 1;
- val gen_term = TermSubst.generalize_option (tfrees, frees) idx;
- val gen_typ = TermSubst.generalizeT_option tfrees idx;
+ val gen_term = Term_Subst.generalize_option (tfrees, frees) idx;
+ val gen_typ = Term_Subst.generalizeT_option tfrees idx;
in Proofterm.map_proof_terms_option gen_term gen_typ prf end;
@@ -411,18 +411,18 @@
let
val ren = Name.clean #> (if is_open then I else Name.internal);
val (instT, ctxt') = importT_inst ts ctxt;
- val vars = map (apsnd (TermSubst.instantiateT instT)) (rev (fold Term.add_vars ts []));
+ val vars = map (apsnd (Term_Subst.instantiateT instT)) (rev (fold Term.add_vars ts []));
val (xs, ctxt'') = variant_fixes (map (ren o #1 o #1) vars) ctxt';
val inst = vars ~~ map Free (xs ~~ map #2 vars);
in ((instT, inst), ctxt'') end;
fun importT_terms ts ctxt =
let val (instT, ctxt') = importT_inst ts ctxt
- in (map (TermSubst.instantiate (instT, [])) ts, ctxt') end;
+ in (map (Term_Subst.instantiate (instT, [])) ts, ctxt') end;
fun import_terms is_open ts ctxt =
let val (inst, ctxt') = import_inst is_open ts ctxt
- in (map (TermSubst.instantiate inst) ts, ctxt') end;
+ in (map (Term_Subst.instantiate inst) ts, ctxt') end;
fun importT ths ctxt =
let
@@ -527,9 +527,9 @@
val idx = maxidx_of ctxt' + 1;
val Ts' = (fold o fold_types o fold_atyps)
(fn T as TFree _ =>
- (case TermSubst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
+ (case Term_Subst.generalizeT types idx T of TVar v => insert (op =) v | _ => I)
| _ => I) ts [];
- val ts' = map (TermSubst.generalize (types, []) idx) ts;
+ val ts' = map (Term_Subst.generalize (types, []) idx) ts;
in (rev Ts', ts') end;
fun polymorphic ctxt ts = snd (polymorphic_types ctxt ts);
--- a/src/Tools/Code/code_preproc.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Fri Jul 10 00:10:36 2009 +0200
@@ -224,7 +224,7 @@
fun default_typscheme_of thy c =
let
- val ty = (snd o dest_Const o TermSubst.zero_var_indexes o curry Const c
+ val ty = (snd o dest_Const o Term_Subst.zero_var_indexes o curry Const c
o Type.strip_sorts o Sign.the_const_type thy) c;
in case AxClass.class_of_param thy c
of SOME class => ([(Name.aT, [class])], ty)
--- a/src/Tools/Compute_Oracle/compute.ML Thu Jul 09 23:05:59 2009 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML Fri Jul 10 00:10:36 2009 +0200
@@ -167,8 +167,6 @@
| machine_of_prog (ProgHaskell _) = HASKELL
| machine_of_prog (ProgSML _) = SML
-structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord)
-
type naming = int -> string
fun default_naming i = "v_" ^ Int.toString i