# HG changeset patch # User wenzelm # Date 1176564967 -7200 # Node ID 31a2303f4283286682a676cc34b01100fdbafddb # Parent 68cd69a388e2789701b098a28d3a45743867fbc1 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; avoid rep_theory; diff -r 68cd69a388e2 -r 31a2303f4283 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Sat Apr 14 17:36:06 2007 +0200 +++ b/src/Pure/codegen.ML Sat Apr 14 17:36:07 2007 +0200 @@ -197,7 +197,7 @@ fun set_default_type s thy ({size, iterations, ...} : test_params) = {size = size, iterations = iterations, - default_type = SOME (typ_of (read_ctyp thy s))}; + default_type = SOME (Sign.read_typ thy s)}; (* data kind 'Pure/codegen' *) @@ -394,7 +394,7 @@ end) (thy, xs); val assoc_consts_i = gen_assoc_consts (K I); -val assoc_consts = gen_assoc_consts (typ_of oo read_ctyp); +val assoc_consts = gen_assoc_consts Sign.read_typ; (**** associate types with target language types ****) @@ -569,8 +569,7 @@ fun mk_deftab thy = let - val axmss = map (fn thy' => - (Context.theory_name thy', snd (#axioms (Theory.rep_theory thy')))) + val axmss = map (fn thy' => (Context.theory_name thy', Theory.axiom_table thy')) (thy :: Theory.ancestors_of thy); fun prep_def def = (case preprocess thy [def] of [def'] => prop_of def' | _ => error "mk_deftab: bad preprocessor"); @@ -911,9 +910,8 @@ (code'', del_nodes [""] gr') end)); -val generate_code_i = gen_generate_code (K I); -val generate_code = gen_generate_code - (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT); +val generate_code_i = gen_generate_code Sign.cert_term; +val generate_code = gen_generate_code Sign.read_term; (**** Reflection ****) @@ -1123,7 +1121,7 @@ (Scan.repeat1 (P.xname --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> (fn xs => Toplevel.theory (fn thy => assoc_types (map (fn ((name, mfx), aux) => (name, (parse_mixfix - (typ_of o read_ctyp thy) mfx, aux))) xs) thy))); + (Sign.read_typ thy) mfx, aux))) xs) thy))); val assoc_constP = OuterSyntax.command "consts_code" @@ -1132,9 +1130,8 @@ (P.xname -- (Scan.option (P.$$$ "::" |-- P.typ)) --| P.$$$ "(" -- P.string --| P.$$$ ")" -- parse_attach) >> (fn xs => Toplevel.theory (fn thy => assoc_consts - (map (fn (((name, optype), mfx), aux) => (name, optype, (parse_mixfix - (term_of o read_cterm thy o rpair TypeInfer.logicT) mfx, aux))) - xs) thy))); + (map (fn (((name, optype), mfx), aux) => + (name, optype, (parse_mixfix (Sign.read_term thy) mfx, aux))) xs) thy))); fun parse_code lib = Scan.optional (P.$$$ "(" |-- P.enum "," P.xname --| P.$$$ ")") (!mode) -- @@ -1183,7 +1180,7 @@ fun parse_tyinst xs = (P.type_ident --| P.$$$ "=" -- P.typ >> (fn (v, s) => fn thy => - fn (x, ys) => (x, (v, typ_of (read_ctyp thy s)) :: ys))) xs; + fn (x, ys) => (x, (v, Sign.read_typ thy s) :: ys))) xs; fun app [] x = x | app (f :: fs) x = app fs (f x);