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:02 +0200
changeset 20077 4fc9a4fef219
parent 20076 def4ad161528
child 20078 f4122d7494f3
replaced Term.variant(list) by Name.variant(_list); Name.clean;
src/Pure/drule.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/drule.ML	Tue Jul 11 12:17:01 2006 +0200
+++ b/src/Pure/drule.ML	Tue Jul 11 12:17:02 2006 +0200
@@ -370,10 +370,8 @@
 val forall_elim_vars = PureThy.forall_elim_vars;
 
 fun outer_params t =
-  let
-    val vs = Term.strip_all_vars t;
-    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;
+  let val vs = Term.strip_all_vars t
+  in Name.variant_list [] (map (Name.clean o #1) vs) ~~ map #2 vs end;
 
 (*generalize outermost parameters*)
 fun gen_all th =
@@ -500,7 +498,7 @@
        [] => (fth, fn x => x)
      | vars =>
          let fun newName (Var(ix,_), (pairs,used)) =
-                   let val v = variant used (string_of_indexname ix)
+                   let val v = Name.variant used (string_of_indexname ix)
                    in  ((ix,v)::pairs, v::used)  end;
              val (alist, _) = foldr newName ([], Library.foldr add_term_names
                (prop :: Thm.terms_of_tpairs tpairs, [])) vars
isabelle