# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1268303557 -3600
# Node ID d3b86738e8484b8f58967191c5fa8f064e94fe44
# Parent  0310a21821a7d99d1b5cff50d100acfb09084f13
Lifting constants works for all examples.

diff -r 0310a21821a7 -r d3b86738e848 Nominal/Parser.thy
--- a/Nominal/Parser.thy	Thu Mar 11 11:25:56 2010 +0100
+++ b/Nominal/Parser.thy	Thu Mar 11 11:32:37 2010 +0100
@@ -303,9 +303,11 @@
   val raw_binds_flat = map (map flat) raw_binds;
   val (((fv_ts_loc, fv_def_loc), alpha), lthy4) = define_fv_alpha dtinfo raw_binds_flat bn_funs_decls lthy3;
   val alpha_ts_loc = #preds alpha
+  val alpha_ts_loc_nobn = List.take (alpha_ts_loc, length perms)
   val morphism_4_3 = ProofContext.export_morphism lthy4 lthy3;
   val fv_ts = map (Morphism.term morphism_4_3) fv_ts_loc;
   val alpha_ts = map (Morphism.term morphism_4_3) alpha_ts_loc;
+  val alpha_ts_nobn = List.take (alpha_ts, length perms)
   val alpha_induct_loc = #induct alpha
   val [alpha_induct] = ProofContext.export lthy4 lthy3 [alpha_induct_loc];
   val alpha_inducts = Project_Rule.projects lthy4 (1 upto (length dts)) alpha_induct
@@ -322,7 +324,7 @@
   fun alpha_eqvt_tac' _ =
     if !cheat_alpha_eqvt then Skip_Proof.cheat_tac thy
     else alpha_eqvt_tac alpha_induct_loc (raw_perm_def @ alpha_inj_loc) lthy4 1
-  val alpha_eqvt_loc = build_alpha_eqvts (List.take (alpha_ts_loc, length perms)) perms alpha_eqvt_tac' lthy4;
+  val alpha_eqvt_loc = build_alpha_eqvts alpha_ts_loc_nobn perms alpha_eqvt_tac' lthy4;
   val alpha_eqvt = ProofContext.export lthy4 lthy2 alpha_eqvt_loc;
   val (bv_eqvts, lthy5) = fold_map (build_bv_eqvt (raw_bn_eqs @ raw_perm_def) inducts) bns lthy4;
   val fv_eqvt_tac =
@@ -331,20 +333,15 @@
   val (fv_eqvts, lthy6) = build_eqvts Binding.empty fv_ts_loc fv_eqvt_tac lthy5;
   val raw_fv_bv_eqvt_loc = flat (map snd bv_eqvts) @ (snd fv_eqvts)
   val raw_fv_bv_eqvt = ProofContext.export lthy6 lthy3 raw_fv_bv_eqvt_loc;
-  val alpha_equivp_loc = map (equivp_hack lthy6) (List.take (alpha_ts_loc, length perms))
+  val alpha_equivp_loc = map (equivp_hack lthy6) alpha_ts_loc_nobn
 (*  val alpha_equivp_loc = build_equivps alpha_ts_loc induct alpha_induct_loc
     inject alpha_inj_loc distinct alpha_cases_loc alpha_eqvt_loc lthy6;*)
   val alpha_equivp = ProofContext.export lthy6 lthy2 alpha_equivp_loc;
   val qty_binds = map (fn (_, b, _, _) => b) dts;
   val qty_names = map Name.of_binding qty_binds;
   val qty_full_names = map (Long_Name.qualify thy_name) qty_names
-in
-if !restricted_nominal = 0 then
-  ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy6)
-else
-let
   val lthy7 = define_quotient_type
-    (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts))
+    (map (fn ((b, t), alpha) => (([], b, NoSyn), (t, alpha))) ((qty_binds ~~ all_typs) ~~ alpha_ts_nobn))
     (ALLGOALS (resolve_tac alpha_equivp)) lthy6;
   val const_names = map Name.of_binding (flat (map (fn (_, _, _, t) => map (fn (b, _, _) => b) t) dts));
   val raw_consts =
@@ -355,7 +352,7 @@
   val (consts_defs, lthy8) = fold_map Quotient_Def.quotient_lift_const (const_names ~~ raw_consts) lthy7;
   val (consts, const_defs) = split_list consts_defs;
 in
-if !restricted_nominal = 1 then
+if !restricted_nominal = 0 then
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy8)
 else
 let
@@ -401,7 +398,6 @@
   ((raw_dt_names, raw_bn_funs, raw_bn_eqs, raw_binds), lthy20)
 end
 end
-end
 *}
 
 ML {*