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.
tuned name generation code (to make it easier to adapt later)
authorblanchet
Fri, 09 Aug 2013 15:40:38 +0200
changeset 52938 3b3e52d5e66b
parent 52937 cdd1d5049287
child 52950 9a65588c0118
tuned name generation code (to make it easier to adapt later)
src/HOL/BNF/Tools/bnf_gfp.ML file | annotate | diff | comparison | revisions
src/HOL/BNF/Tools/bnf_lfp.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Aug 09 15:03:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Fri Aug 09 15:40:38 2013 +0200
@@ -72,19 +72,21 @@
     val names_lthy = fold Variable.declare_typ deads lthy;
 
     (* tvars *)
-    val ((((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
-      (passiveCs, activeCs)), passiveXs), passiveYs), idxT) = names_lthy
-      |> mk_TFrees live
-      |> apfst (`(chop m))
-      ||> mk_TFrees live
-      ||>> apfst (`(chop m))
-      ||> mk_TFrees live
-      ||>> apfst (chop m)
+    val ((((((((passiveAs, activeAs), passiveBs), activeBs), passiveCs), activeCs), passiveXs),
+        passiveYs), idxT) = names_lthy
+      |> mk_TFrees m
+      ||>> mk_TFrees n
+      ||>> mk_TFrees m
+      ||>> mk_TFrees n
+      ||>> mk_TFrees m
+      ||>> mk_TFrees n
       ||>> mk_TFrees m
       ||>> mk_TFrees m
       ||> fst o mk_TFrees 1
       ||> the_single;
 
+    val allAs = passiveAs @ activeAs;
+    val allBs' = passiveBs @ activeBs;
     val Ass = replicate n allAs;
     val allBs = passiveAs @ activeBs;
     val Bss = replicate n allBs;
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Aug 09 15:03:39 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Fri Aug 09 15:40:38 2013 +0200
@@ -42,16 +42,18 @@
     val names_lthy = fold Variable.declare_typ deads lthy;
 
     (* tvars *)
-    val (((((((passiveAs, activeAs), allAs)), ((passiveBs, activeBs), allBs')),
-      activeCs), passiveXs), passiveYs) = names_lthy
-      |> mk_TFrees live
-      |> apfst (`(chop m))
-      ||> mk_TFrees live
-      ||>> apfst (`(chop m))
+    val ((((((passiveAs, activeAs), passiveBs), activeBs), activeCs), passiveXs), passiveYs) =
+      names_lthy
+      |> mk_TFrees m
+      ||>> mk_TFrees n
+      ||>> mk_TFrees m
+      ||>> mk_TFrees n
       ||>> mk_TFrees n
       ||>> mk_TFrees m
       ||> fst o mk_TFrees m;
 
+    val allAs = passiveAs @ activeAs;
+    val allBs' = passiveBs @ activeBs;
     val Ass = replicate n allAs;
     val allBs = passiveAs @ activeBs;
     val Bss = replicate n allBs;
isabelle