Term.internal;
authorwenzelm
Sat, 17 Jun 2006 19:37:47 +0200
changeset 19906 c23a0e65b285
parent 19905 7f480338b66e
child 19907 f552697b2f19
Term.internal;
src/Pure/Isar/obtain.ML
src/Pure/drule.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 []
--- 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);