--- a/src/Pure/Isar/obtain.ML Sat Jun 17 19:37:46 2006 +0200
+++ b/src/Pure/Isar/obtain.ML Sat Jun 17 19:37:47 2006 +0200
@@ -200,7 +200,7 @@
val xs = map (apsnd norm_type) vars;
val ys = map (apsnd norm_type) (Library.drop (m, params));
- val ys' = map Syntax.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys;
+ val ys' = map Term.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys;
val instT =
fold (Term.add_tvarsT o #2) params []
--- a/src/Pure/drule.ML Sat Jun 17 19:37:46 2006 +0200
+++ b/src/Pure/drule.ML Sat Jun 17 19:37:47 2006 +0200
@@ -373,7 +373,7 @@
fun outer_params t =
let
val vs = Term.strip_all_vars t;
- val clean_name = perhaps (try Syntax.dest_skolem) #> perhaps (try Syntax.dest_internal);
+ val clean_name = perhaps (try Term.dest_skolem) #> perhaps (try Term.dest_internal);
in Term.variantlist (map (clean_name o #1) vs, []) ~~ map #2 vs end;
(*generalize outermost parameters*)
@@ -1088,7 +1088,7 @@
(gen_rems (op = o apfst fst) (tfrees_of thm, tfrees)) thm);
-(* increment var indexes *)
+(* var indexes *)
fun incr_indexes th = Thm.incr_indexes (Thm.maxidx_of th + 1);