# HG changeset patch
# User berghofe
# Date 1133026901 -3600
# Node ID 1318955d57ac3f04826bdcaf811b9d1a36ecf254
# Parent  5597cfcecd49dbd6ecc96e6269e3012404d76b62
Corrected treatment of non-recursive abstraction types.

diff -r 5597cfcecd49 -r 1318955d57ac src/HOL/Nominal/nominal_package.ML
--- a/src/HOL/Nominal/nominal_package.ML	Fri Nov 25 21:14:34 2005 +0100
+++ b/src/HOL/Nominal/nominal_package.ML	Sat Nov 26 18:41:41 2005 +0100
@@ -398,6 +398,8 @@
              SOME ("nominal.nOption", _, [(_, [dt']), _]) =>
                apfst (cons dt) (strip_option dt')
            | _ => ([], dtf))
+      | strip_option (DtType ("fun", [dt, DtType ("nominal.nOption", [dt'])])) =
+          apfst (cons dt) (strip_option dt')
       | strip_option dt = ([], dt);
 
     fun make_intr s T (cname, cargs) =
@@ -640,17 +642,17 @@
               (dts ~~ (j upto j + length dts - 1))
             val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts)
             val (dts', dt'') = strip_dtyp dt'
-          in case dt'' of
-              DtRec k => if k < length new_type_names then
-                  (j + length dts + 1,
-                   xs @ x :: l_args,
-                   foldr mk_abs_fun
-                     (list_abs (map (pair "z" o typ_of_dtyp') dts',
-                       Const (List.nth (rep_names, k), typ_of_dtyp' dt'' -->
-                         typ_of_dtyp descr sorts' dt'') $ app_bnds x (length dts')))
-                     xs :: r_args)
-                else error "nested recursion not (yet) supported"
-            | _ => (j + 1, x' :: l_args, x' :: r_args)
+          in
+            (j + length dts + 1,
+             xs @ x :: l_args,
+             foldr mk_abs_fun
+               (case dt'' of
+                  DtRec k => if k < length new_type_names then
+                      list_abs (map (pair "z" o typ_of_dtyp') dts',
+                        Const (List.nth (rep_names, k), typ_of_dtyp' dt'' -->
+                          typ_of_dtyp descr sorts' dt'') $ app_bnds x (length dts'))
+                    else error "nested recursion not (yet) supported"
+                | _ => x) xs :: r_args)
           end
 
         val (_, l_args, r_args) = foldr constr_arg (1, [], []) cargs;
@@ -780,13 +782,10 @@
                 (Ts ~~ (j upto j + length dts - 1))
               val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
               val (dts', dt'') = strip_dtyp dt';
-            in case dt'' of
-                DtRec k => if k < length new_type_names then
-                    (j + length dts + 1,
-                     xs @ x :: l_args,
-                     map perm (xs @ [x]) @ r_args)
-                  else error "nested recursion not (yet) supported"
-              | _ => (j + 1, x' :: l_args, perm x' :: r_args)
+            in
+              (j + length dts + 1,
+               xs @ x :: l_args,
+               map perm (xs @ [x]) @ r_args)
             end
 
           val (_, l_args, r_args) = foldr constr_arg (1, [], []) dts;
@@ -834,14 +833,11 @@
               val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
               val y = mk_Free "y" (typ_of_dtyp' dt') (j + length dts);
               val (dts', dt'') = strip_dtyp dt';
-            in case dt'' of
-                DtRec k => if k < length new_type_names then
-                    (j + length dts + 1,
-                     xs @ (x :: args1), ys @ (y :: args2),
-                     HOLogic.mk_eq
-                       (foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs)
-                  else error "nested recursion not (yet) supported"
-              | _ => (j + 1, x' :: args1, y' :: args2, HOLogic.mk_eq (x', y') :: eqs)
+            in
+              (j + length dts + 1,
+               xs @ (x :: args1), ys @ (y :: args2),
+               HOLogic.mk_eq
+                 (foldr mk_abs_fun x xs, foldr mk_abs_fun y ys) :: eqs)
             end;
 
           val (_, args1, args2, eqs) = foldr make_inj (1, [], [], []) dts;
@@ -886,12 +882,9 @@
               val xs = map (fn (T, i) => mk_Free "x" T i) Ts_idx;
               val x = mk_Free "x" (typ_of_dtyp' dt') (j + length dts);
               val (dts', dt'') = strip_dtyp dt';
-            in case dt'' of
-                DtRec k => if k < length new_type_names then
-                    (j + length dts + 1,
-                     xs @ (x :: args1), foldr mk_abs_fun x xs :: args2)
-                  else error "nested recursion not (yet) supported"
-              | _ => (j + 1, x' :: args1, x' :: args2)
+            in
+              (j + length dts + 1,
+               xs @ (x :: args1), foldr mk_abs_fun x xs :: args2)
             end;
 
           val (_, args1, args2) = foldr process_constr (1, [], []) dts;
@@ -1004,8 +997,6 @@
     val abs_supp = PureThy.get_thms thy8 (Name "abs_supp");
     val supp_atm = PureThy.get_thms thy8 (Name "supp_atm");
 
-
-(*
     val finite_supp_thms = map (fn atom =>
       let val atomT = Type (atom, [])
       in map standard (List.take
@@ -1021,7 +1012,6 @@
                List.concat supp_thms))))),
          length new_type_names))
       end) atoms;
-*)
 
     (**** strong induction theorem ****)
 
@@ -1086,13 +1076,13 @@
       DatatypeAux.store_thmss "inject" new_type_names inject_thms |>>>
       DatatypeAux.store_thmss "supp" new_type_names supp_thms |>>>
       DatatypeAux.store_thmss_atts "fresh" new_type_names simp_atts fresh_thms |>>
-  (*    fold (fn (atom, ths) => fn thy =>
+      fold (fn (atom, ths) => fn thy =>
         let val class = Sign.intern_class thy ("fs_" ^ Sign.base_name atom)
         in fold (fn T => AxClass.add_inst_arity_i
             (fst (dest_Type T),
               replicate (length sorts) [class], [class])
             (AxClass.intro_classes_tac [] THEN resolve_tac ths 1)) newTs thy
-        end) (atoms ~~ finite_supp_thms) |>> *)
+        end) (atoms ~~ finite_supp_thms) |>>
       Theory.add_path big_name |>>>
       PureThy.add_axioms_i [(("induct_unsafe", induct), [case_names_induct])] |>>
       Theory.parent_path;
@@ -1127,4 +1117,5 @@
 
 end;
 
-end
\ No newline at end of file
+end
+