# HG changeset patch
# User wenzelm
# Date 1150565867 -7200
# Node ID c23a0e65b285bfd943f07fe090b07c13054444cf
# Parent  7f480338b66e11ebdfc3700d726d78abd4eca6bb
Term.internal;

diff -r 7f480338b66e -r c23a0e65b285 src/Pure/Isar/obtain.ML
--- 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 []
diff -r 7f480338b66e -r c23a0e65b285 src/Pure/drule.ML
--- 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);