Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/inductive_package.ML
changeset 16287 7a03b4b4df67
parent 16122 864fda4a4056
child 16364 dc9f7066d80a 
--- a/src/HOL/Tools/inductive_package.ML	Sun Jun 05 23:07:24 2005 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sun Jun 05 23:07:25 2005 +0200
@@ -193,8 +193,7 @@
           (env, (replicate (length consts) cT) ~~ consts)
       end;
     val (env, _) = Library.foldl unify ((Vartab.empty, i'), rec_consts);
-    val subst = fst o Type.freeze_thaw o
-      (map_term_types (Envir.norm_type env))
+    val subst = Type.freeze o map_term_types (Envir.norm_type env)
 
   in (map subst cs', map subst intr_ts')
   end) handle Type.TUNIFY =>
isabelle