# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1267532934 -3600
# Node ID d3101a5b9c4d418a4df0196934cec62aa611026a
# Parent  c145c380e19550656784f40669fca346fe0212ef
Length fix for nested recursions.

diff -r c145c380e195 -r d3101a5b9c4d Nominal/Fv.thy
--- a/Nominal/Fv.thy	Tue Mar 02 12:28:07 2010 +0100
+++ b/Nominal/Fv.thy	Tue Mar 02 13:28:54 2010 +0100
@@ -54,6 +54,13 @@
       in the database.
 *)
 
+ML {*
+fun map2i _ [] [] = []
+  | map2i f (x :: xs) (y :: ys) = f x y :: map2i f xs ys
+  | map2i f (x :: xs) [] = f x [] :: map2i f xs []
+  | map2i _ _ _ = raise UnequalLengths;
+*}
+
 (* TODO: should be const_name union *)
 ML {*
   open Datatype_Aux; (* typ_of_dtyp, DtRec, ... *);
@@ -185,8 +192,8 @@
     in
       (fv_eq, alpha_eq)
     end;
-  fun fv_alpha_eq (i, (_, _, constrs)) binds = map2 (fv_alpha_constr i) constrs binds;
-  val (fv_eqs, alpha_eqs) = split_list (flat (map2 fv_alpha_eq descr bindsall))
+  fun fv_alpha_eq (i, (_, _, constrs)) binds = map2i (fv_alpha_constr i) constrs binds;
+  val (fv_eqs, alpha_eqs) = split_list (flat (map2i fv_alpha_eq descr bindsall))
   val add_binds = map (fn x => (Attrib.empty_binding, x))
   val (fvs, lthy') = (Primrec.add_primrec
     (map (fn s => (Binding.name s, NONE, NoSyn)) fv_names) (add_binds fv_eqs) lthy)
diff -r c145c380e195 -r d3101a5b9c4d Nominal/Test.thy
--- a/Nominal/Test.thy	Tue Mar 02 12:28:07 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 02 13:28:54 2010 +0100
@@ -68,12 +68,12 @@
 
 text {* example type schemes *}
 
-(* does not work yet 
-nominal_datatype t = 
-  Var "name" 
+nominal_datatype t =
+  Var "name"
 | Fun "t" "t"
 
-nominal_datatype tyS = 
+(* does not work yet
+nominal_datatype tyS =
   All xs::"name list" ty::"t_raw" bind xs in ty
 *)
 
@@ -137,12 +137,12 @@
 
 (* example 4 from Terms.thy *)
 
-(* does not work yet
+
 nominal_datatype trm4 =
   Vr4 "name"
 | Ap4 "trm4" "trm4 list"
 | Lm4 x::"name" t::"trm4"  bind x in t
-*)
+
 
 (* example 5 from Terms.thy *)