Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
replaced Term.variant(list) by Name.variant(_list);
authorwenzelm
Tue, 11 Jul 2006 12:17:11 +0200
changeset 20085 c5d60752587f
parent 20084 aa320957f00c
child 20086 94ca946fb689
replaced Term.variant(list) by Name.variant(_list); Name.internal;
src/Pure/Isar/obtain.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/obtain.ML	Tue Jul 11 12:17:09 2006 +0200
+++ b/src/Pure/Isar/obtain.ML	Tue Jul 11 12:17:11 2006 +0200
@@ -120,7 +120,7 @@
     val _ = Variable.warn_extra_tfrees fix_ctxt asms_ctxt;
 
     (*obtain statements*)
-    val thesisN = Term.variant xs AutoBind.thesisN;
+    val thesisN = Name.variant xs AutoBind.thesisN;
     val (thesis_var, thesis) = bind_judgment fix_ctxt thesisN;
 
     fun occs_var x = Library.get_first (fn t =>
@@ -196,7 +196,7 @@
 
     val xs = map (apsnd norm_type o fst) vars;
     val ys = map (apsnd norm_type) (Library.drop (m, params));
-    val ys' = map Term.internal (Term.variantlist (map fst ys, map fst xs)) ~~ map #2 ys;
+    val ys' = map Name.internal (Name.variant_list (map fst xs) (map fst ys)) ~~ map #2 ys;
     val terms = map (Drule.mk_term o cert o Free) (xs @ ys');
 
     val instT =
isabelle