# HG changeset patch # User Cezary Kaliszyk # Date 1272879338 -7200 # Node ID f494d5a67564f5040d4a2921ce6400d2fb7d8557 # Parent 6a4049e1d68d67fb0af231b267f7ee98c0eef512 Fix Parser diff -r 6a4049e1d68d -r f494d5a67564 Nominal/Parser.thy --- a/Nominal/Parser.thy Mon May 03 10:15:23 2010 +0200 +++ b/Nominal/Parser.thy Mon May 03 11:35:38 2010 +0200 @@ -1,8 +1,8 @@ theory Parser -imports "../Nominal-General/Nominal2_Atoms" - "../Nominal-General/Nominal2_Eqvt" - "../Nominal-General/Nominal2_Supp" - "Perm" "Equivp" "Rsp" "Lift" +imports "../Nominal-General/Nominal2_Atoms" + "../Nominal-General/Nominal2_Eqvt" + "../Nominal-General/Nominal2_Supp" + "Perm" "Equivp" "Rsp" "Lift" "Fv" begin section{* Interface for nominal_datatype *} @@ -372,9 +372,9 @@ val dtinfo = Datatype.the_info (ProofContext.theory_of lthy2) (hd raw_dt_names); val {descr, sorts, ...} = dtinfo; - fun nth_dtyp i = typ_of_dtyp descr sorts (DtRec i); + fun nth_dtyp i = Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i); val raw_tys = map (fn (i, _) => nth_dtyp i) descr; - val all_typs = map (fn i => typ_of_dtyp descr sorts (DtRec i)) (map fst descr) + val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; val dtinfos = map (Datatype.the_info (ProofContext.theory_of lthy2)) all_full_tnames; val rel_dtinfos = List.take (dtinfos, (length dts)); @@ -423,8 +423,8 @@ val raw_consts = flat (map (fn (i, (_, _, l)) => map (fn (cname, dts) => - Const (cname, map (typ_of_dtyp descr sorts) dts ---> - typ_of_dtyp descr sorts (DtRec i))) l) descr); + Const (cname, map (Datatype_Aux.typ_of_dtyp descr sorts) dts ---> + Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i))) l) descr); val (consts, const_defs, lthy8) = quotient_lift_consts_export qtys (const_names ~~ raw_consts) lthy7; val _ = tracing "Proving respects"; val bns_rsp_pre' = build_fvbv_rsps alpha_ts alpha_induct raw_bn_eqs (map fst bns) lthy8;