diff -r 77f448727bf9 -r 58e60df1ff79 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Sat Aug 21 20:07:52 2010 +0800 +++ b/Nominal/NewParser.thy Sun Aug 22 11:00:53 2010 +0800 @@ -566,7 +566,7 @@ fun suffix_bind s = Binding.qualify true q_name (Binding.name s); val _ = warning "Lifting induction"; val constr_names = map (Long_Name.base_name o fst o dest_Const) qconstrs; - val q_induct = Rule_Cases.name constr_names (lift_thm qtys lthy13 raw_induct_thm); + val q_induct = Rule_Cases.name constr_names (lift_thm lthy13 qtys raw_induct_thm); fun note_suffix s th ctxt = snd (Local_Theory.note ((suffix_bind s, []), th) ctxt); fun note_simp_suffix s th ctxt = @@ -576,24 +576,24 @@ [Rule_Cases.name constr_names q_induct]) lthy13; val q_inducts = Project_Rule.projects lthy13 (1 upto (length raw_fvs)) q_induct val (_, lthy14a) = Local_Theory.note ((suffix_bind "inducts", []), q_inducts) lthy14; - val q_perm = map (lift_thm qtys lthy14) raw_perm_simps; + val q_perm = map (lift_thm lthy14 qtys) raw_perm_simps; val lthy15 = note_simp_suffix "perm" q_perm lthy14a; - val q_fv = map (lift_thm qtys lthy15) raw_fv_defs; + val q_fv = map (lift_thm lthy15 qtys) raw_fv_defs; val lthy16 = note_simp_suffix "fv" q_fv lthy15; - val q_bn = map (lift_thm qtys lthy16) raw_bn_defs; + val q_bn = map (lift_thm lthy16 qtys) raw_bn_defs; val lthy17 = note_simp_suffix "bn" q_bn lthy16; val _ = warning "Lifting eq-iff"; (*val _ = map tracing (map PolyML.makestring alpha_eq_iff);*) val eq_iff_unfolded0 = map (Local_Defs.unfold lthy17 @{thms alphas}) alpha_eq_iff val eq_iff_unfolded1 = map (Local_Defs.unfold lthy17 @{thms Pair_eqvt}) eq_iff_unfolded0 - val q_eq_iff_pre0 = map (lift_thm qtys lthy17) eq_iff_unfolded1; + val q_eq_iff_pre0 = map (lift_thm lthy17 qtys) eq_iff_unfolded1; val q_eq_iff_pre1 = map (Local_Defs.fold lthy17 @{thms Pair_eqvt}) q_eq_iff_pre0 val q_eq_iff_pre2 = map (Local_Defs.fold lthy17 @{thms alphas}) q_eq_iff_pre1 val q_eq_iff = map (Local_Defs.unfold lthy17 (Quotient_Info.id_simps_get lthy17)) q_eq_iff_pre2 val (_, lthy18) = Local_Theory.note ((suffix_bind "eq_iff", []), q_eq_iff) lthy17; - val q_dis = map (lift_thm qtys lthy18) alpha_distincts; + val q_dis = map (lift_thm lthy18 qtys) alpha_distincts; val lthy19 = note_simp_suffix "distinct" q_dis lthy18; - val q_eqvt = map (lift_thm qtys lthy19) (raw_bn_eqvt @ raw_fv_eqvt); + val q_eqvt = map (lift_thm lthy19 qtys) (raw_bn_eqvt @ raw_fv_eqvt); val (_, lthy20) = Local_Theory.note ((Binding.empty, [Attrib.internal (fn _ => Nominal_ThmDecls.eqvt_add)]), q_eqvt) lthy19; val _ = warning "Supports";