# HG changeset patch # User haftmann # Date 1242054511 -7200 # Node ID ee45b1c733c16b08c779d89afbcdad2ccdf808c1 # Parent 3e69a25b90a238452f9838725378fa68f95fc825# Parent 27a6558e64b62aef9feffcb77f38b410ee4fabf2 merged diff -r 3e69a25b90a2 -r ee45b1c733c1 src/HOL/Library/Efficient_Nat.thy --- a/src/HOL/Library/Efficient_Nat.thy Mon May 11 15:05:17 2009 +0100 +++ b/src/HOL/Library/Efficient_Nat.thy Mon May 11 17:08:31 2009 +0200 @@ -179,10 +179,8 @@ else NONE end; -fun eqn_suc_preproc thy = map fst - #> gen_eqn_suc_preproc - @{thm Suc_if_eq} I (fst o Logic.dest_equals) thy - #> (Option.map o map) (Code_Unit.mk_eqn thy); +val eqn_suc_preproc = Code.simple_functrans (gen_eqn_suc_preproc + @{thm Suc_if_eq} I (fst o Logic.dest_equals)); fun eqn_suc_preproc' thy thms = gen_eqn_suc_preproc @{thm Suc_if_eq'} (snd o Thm.dest_comb) (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) thy thms diff -r 3e69a25b90a2 -r ee45b1c733c1 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Mon May 11 15:05:17 2009 +0100 +++ b/src/HOL/Tools/recfun_codegen.ML Mon May 11 17:08:31 2009 +0200 @@ -25,13 +25,13 @@ fun add_thm NONE thm thy = Code.add_eqn thm thy | add_thm (SOME module_name) thm thy = - case Code_Unit.warning_thm (Code_Unit.mk_eqn thy) thm - of SOME (thm', _) => let val c = Code_Unit.const_eqn thm' - in thy - |> ModuleData.map (Symtab.update (c, module_name)) - |> Code.add_eqn thm' - end - | NONE => Code.add_eqn thm thy; + let + val (thm', _) = Code_Unit.mk_eqn thy (K false) (thm, true) + in + thy + |> ModuleData.map (Symtab.update (Code_Unit.const_eqn thy thm', module_name)) + |> Code.add_eqn thm' + end; fun meta_eq_to_obj_eq thy thm = let @@ -57,7 +57,6 @@ val thms = Code.these_raw_eqns thy c' |> map_filter (fn (thm, linear) => if linear then SOME thm else NONE) |> expand_eta thy - |> map (AxClass.overload thy) |> map_filter (meta_eq_to_obj_eq thy) |> Code_Unit.norm_varnames thy |> map (rpair opt_name) diff -r 3e69a25b90a2 -r ee45b1c733c1 src/HOL/Tools/typecopy_package.ML --- a/src/HOL/Tools/typecopy_package.ML Mon May 11 15:05:17 2009 +0100 +++ b/src/HOL/Tools/typecopy_package.ML Mon May 11 17:08:31 2009 +0200 @@ -150,7 +150,7 @@ THEN ALLGOALS (rtac @{thm refl})) def_thm) |-> (fn def_thm => Code.add_eqn def_thm) |> `(fn thy => mk_eq_refl thy) - |-> (fn refl_thm => Code.add_nonlinear_eqn refl_thm) + |-> (fn refl_thm => Code.add_nbe_eqn refl_thm) end; val setup = diff -r 3e69a25b90a2 -r ee45b1c733c1 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon May 11 15:05:17 2009 +0100 +++ b/src/Pure/Isar/code.ML Mon May 11 17:08:31 2009 +0200 @@ -8,7 +8,7 @@ signature CODE = sig val add_eqn: thm -> theory -> theory - val add_nonlinear_eqn: thm -> theory -> theory + val add_nbe_eqn: thm -> theory -> theory val add_default_eqn: thm -> theory -> theory val add_default_eqn_attribute: attribute val add_default_eqn_attrib: Attrib.src @@ -20,6 +20,8 @@ val add_inline: thm -> theory -> theory val add_functrans: string * (theory -> (thm * bool) list -> (thm * bool) list option) -> theory -> theory val del_functrans: string -> theory -> theory + val simple_functrans: (theory -> thm list -> thm list option) + -> theory -> (thm * bool) list -> (thm * bool) list option val add_datatype: (string * typ) list -> theory -> theory val add_datatype_cmd: string list -> theory -> theory val type_interpretation: @@ -109,7 +111,7 @@ (* code equations *) type eqns = bool * (thm * bool) list lazy; - (*default flag, theorems with linear flag (perhaps lazy)*) + (*default flag, theorems with proper flag (perhaps lazy)*) fun pretty_lthms ctxt r = case Lazy.peek r of SOME thms => map (ProofContext.pretty_thm ctxt o fst) (Exn.release thms) @@ -122,18 +124,18 @@ val thy_ref = Theory.check_thy thy; in Lazy.lazy (fn () => (f (Theory.deref thy_ref) o Lazy.force) r) end; -fun add_drop_redundant thy (thm, linear) thms = +fun add_drop_redundant thy (thm, proper) thms = let val args_of = snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; val args = args_of thm; val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1); fun matches_args args' = length args <= length args' andalso Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args'); - fun drop (thm', linear') = if (linear orelse not linear') + fun drop (thm', proper') = if (proper orelse not proper') andalso matches_args (args_of thm') then (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true) else false; - in (thm, linear) :: filter_out drop thms end; + in (thm, proper) :: filter_out drop thms end; fun add_thm thy _ thm (false, thms) = (false, Lazy.map_force (add_drop_redundant thy thm) thms) | add_thm thy true thm (true, thms) = (true, Lazy.map_force (fn thms => thms @ [thm]) thms) @@ -456,16 +458,6 @@ cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env []; in map (Thm.instantiate (instT, [])) thms' end; -fun check_linear (eqn as (thm, linear)) = - if linear then eqn else Code_Unit.bad_thm - ("Duplicate variables on left hand side of code equation:\n" - ^ Display.string_of_thm thm); - -fun mk_eqn thy linear = - Code_Unit.error_thm ((if linear then check_linear else I) o Code_Unit.mk_eqn thy); -fun mk_syntactic_eqn thy = Code_Unit.warning_thm (Code_Unit.mk_eqn thy); -fun mk_default_eqn thy = Code_Unit.try_thm (check_linear o Code_Unit.mk_eqn thy); - (** interfaces and attributes **) @@ -487,51 +479,47 @@ then SOME tyco else NONE | _ => NONE; -fun recheck_eqn thy = Code_Unit.error_thm - (Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy)); +fun is_constr thy = is_some o get_datatype_of_constr thy; + +fun assert_eqn thy = Code_Unit.assert_eqn thy (is_constr thy); -fun recheck_eqns_const thy c eqns = +fun assert_eqns_const thy c eqns = let - fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm + fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thy thm then eqn else error ("Wrong head of code equation,\nexpected constant " ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm) - in map (cert o recheck_eqn thy) eqns end; + in map (cert o assert_eqn thy) eqns end; fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), []))) o apfst) (fn (_, eqns) => (true, f eqns)); -fun gen_add_eqn linear default thm thy = - case (if default then mk_default_eqn thy else SOME o mk_eqn thy linear) thm - of SOME (thm, _) => - let - val c = Code_Unit.const_eqn thm; - val _ = if not default andalso (is_some o AxClass.class_of_param thy) c - then error ("Rejected polymorphic code equation for overloaded constant:\n" - ^ Display.string_of_thm thm) - else (); - val _ = if not default andalso (is_some o get_datatype_of_constr thy) c - then error ("Rejected code equation for datatype constructor:\n" - ^ Display.string_of_thm thm) - else (); - in change_eqns false c (add_thm thy default (thm, linear)) thy end +fun gen_add_eqn default (eqn as (thm, _)) thy = + let val c = Code_Unit.const_eqn thy thm + in change_eqns false c (add_thm thy default eqn) thy end; + +fun add_eqn thm thy = + gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, true)) thy; + +fun add_default_eqn thm thy = + case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm + of SOME eqn => gen_add_eqn true eqn thy | NONE => thy; -val add_eqn = gen_add_eqn true false; -val add_default_eqn = gen_add_eqn true true; -val add_nonlinear_eqn = gen_add_eqn false false; +fun add_nbe_eqn thm thy = + gen_add_eqn false (Code_Unit.mk_eqn thy (is_constr thy) (thm, false)) thy; fun add_eqnl (c, lthms) thy = let - val lthms' = certificate thy (fn thy => recheck_eqns_const thy c) lthms; + val lthms' = certificate thy (fn thy => assert_eqns_const thy c) lthms; in change_eqns false c (add_lthms lthms') thy end; val add_default_eqn_attribute = Thm.declaration_attribute (fn thm => Context.mapping (add_default_eqn thm) I); val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute); -fun del_eqn thm thy = case mk_syntactic_eqn thy thm - of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thm) (del_thm thm) thy +fun del_eqn thm thy = case Code_Unit.mk_eqn_liberal thy (is_constr thy) thm + of SOME (thm, _) => change_eqns true (Code_Unit.const_eqn thy thm) (del_thm thm) thy | NONE => thy; fun del_eqns c = change_eqns true c (K (false, Lazy.value [])); @@ -553,9 +541,9 @@ then insert (op =) c else I) cases []) cases; in thy + |> fold (del_eqns o fst) cs |> map_exec_purge NONE ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos)) - #> map_eqns (fold (Symtab.delete_safe o fst) cs) #> (map_cases o apfst) drop_outdated_cases) |> TypeInterpretation.data (tyco, serial ()) end; @@ -571,7 +559,7 @@ fun add_case thm thy = let val (c, (k, case_pats)) = Code_Unit.case_cert thm; - val _ = case filter (is_none o get_datatype_of_constr thy) case_pats + val _ = case filter_out (is_constr thy) case_pats of [] => () | cs => error ("Non-constructor(s) in case certificate: " ^ commas (map quote cs)); val entry = (1 + Int.max (1, length case_pats), (k, case_pats)) @@ -596,6 +584,10 @@ (map_exec_purge NONE o map_thmproc o apsnd) (delete_force "function transformer" name); +fun simple_functrans f thy eqns = case f thy (map fst eqns) + of SOME thms' => SOME (map (rpair (forall snd eqns)) thms') + | NONE => NONE; + val _ = Context.>> (Context.map_theory (let fun mk_attribute f = Thm.declaration_attribute (fn thm => Context.mapping (f thm) I); @@ -607,7 +599,7 @@ in TypeInterpretation.init #> add_del_attribute ("", (add_eqn, del_eqn)) - #> add_simple_attribute ("nbe", add_nonlinear_eqn) + #> add_simple_attribute ("nbe", add_nbe_eqn) #> add_del_attribute ("inline", (add_inline, del_inline)) #> add_del_attribute ("post", (add_post, del_post)) end)); @@ -621,9 +613,7 @@ | apply_functrans thy c [] eqns = eqns | apply_functrans thy c functrans eqns = eqns |> perhaps (perhaps_loop (perhaps_apply functrans)) - |> (map o apfst) (AxClass.unoverload thy) - |> recheck_eqns_const thy c - |> (map o apfst) (AxClass.overload thy); + |> assert_eqns_const thy c; fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm); @@ -634,16 +624,17 @@ #> Logic.dest_equals #> snd; -fun preprocess thy functrans c eqns = +fun preprocess thy c eqns = let val pre = (Simplifier.theory_context thy o #pre o the_thmproc o the_exec) thy; + val functrans = (map (fn (_, (_, f)) => f thy) o #functrans + o the_thmproc o the_exec) thy; in eqns - |> (map o apfst) (AxClass.overload thy) |> apply_functrans thy c functrans |> (map o apfst) (Code_Unit.rewrite_eqn pre) |> (map o apfst) (AxClass.unoverload thy) - |> map (recheck_eqn thy) + |> map (assert_eqn thy) |> burrow_fst (common_typ_eqns thy) end; @@ -677,14 +668,9 @@ |> burrow_fst (common_typ_eqns thy); fun these_eqns thy c = - let - val functrans = (map (fn (_, (_, f)) => f thy) o #functrans - o the_thmproc o the_exec) thy; - in - get_eqns thy c - |> (map o apfst) (Thm.transfer thy) - |> preprocess thy functrans c - end; + get_eqns thy c + |> (map o apfst) (Thm.transfer thy) + |> preprocess thy c; fun default_typscheme thy c = let @@ -693,10 +679,10 @@ fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty); in case AxClass.class_of_param thy c of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c)) - | NONE => if is_some (get_datatype_of_constr thy c) + | NONE => if is_constr thy c then strip_sorts (the_const_typscheme c) else case get_eqns thy c - of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm)) + of (thm, _) :: _ => (Code_Unit.typscheme_eqn thy o Drule.zero_var_indexes) thm | [] => strip_sorts (the_const_typscheme c) end; end; (*local*) diff -r 3e69a25b90a2 -r ee45b1c733c1 src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Mon May 11 15:05:17 2009 +0100 +++ b/src/Pure/Isar/code_unit.ML Mon May 11 17:08:31 2009 +0200 @@ -6,12 +6,6 @@ signature CODE_UNIT = sig - (*generic non-sense*) - val bad_thm: string -> 'a - val error_thm: ('a -> 'b) -> 'a -> 'b - val warning_thm: ('a -> 'b) -> 'a -> 'b option - val try_thm: ('a -> 'b) -> 'a -> 'b option - (*typ instantiations*) val typscheme: theory -> string * typ -> (string * sort) list * typ val inst_thm: theory -> sort Vartab.table -> thm -> thm @@ -35,12 +29,12 @@ -> string * ((string * sort) list * (string * typ list) list) (*code equations*) - val assert_eqn: theory -> thm -> thm - val mk_eqn: theory -> thm -> thm * bool - val assert_linear: (string -> bool) -> thm * bool -> thm * bool - val const_eqn: thm -> string - val const_typ_eqn: thm -> string * typ - val head_eqn: theory -> thm -> string * ((string * sort) list * typ) + val mk_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool + val mk_eqn_liberal: theory -> (string -> bool) -> thm -> (thm * bool) option + val assert_eqn: theory -> (string -> bool) -> thm * bool -> thm * bool + val const_eqn: theory -> thm -> string + val const_typ_eqn: thm -> string * typ + val typscheme_eqn: theory -> thm -> (string * sort) list * typ val expand_eta: theory -> int -> thm -> thm val rewrite_eqn: simpset -> thm -> thm val rewrite_head: thm list -> thm -> thm @@ -57,13 +51,6 @@ (* auxiliary *) -exception BAD_THM of string; -fun bad_thm msg = raise BAD_THM msg; -fun error_thm f thm = f thm handle BAD_THM msg => error msg; -fun warning_thm f thm = SOME (f thm) handle BAD_THM msg - => (warning ("code generator: " ^ msg); NONE); -fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; - fun string_of_typ thy = setmp show_sorts true (Syntax.string_of_typ_global thy); fun string_of_const thy c = case AxClass.inst_of_param thy c of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco) @@ -323,85 +310,96 @@ (* code equations *) -fun assert_eqn thy thm = +exception BAD_THM of string; +fun bad_thm msg = raise BAD_THM msg; +fun error_thm f thm = f thm handle BAD_THM msg => error msg; +fun try_thm f thm = SOME (f thm) handle BAD_THM _ => NONE; + +fun is_linear thm = + let val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm + in not (has_duplicates (op =) ((fold o fold_aterms) + (fn Var (v, _) => cons v | _ => I) args [])) end; + +fun gen_assert_eqn thy is_constr_head is_constr_pat (thm, proper) = let val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm handle TERM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm) - | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm); + | THM _ => bad_thm ("Not an equation: " ^ Display.string_of_thm thm); fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v - | Free _ => bad_thm ("Illegal free variable in rewrite theorem\n" + | Free _ => bad_thm ("Illegal free variable in equation\n" ^ Display.string_of_thm thm) | _ => I) t []; fun tvars_of t = fold_term_types (fn _ => fold_atyps (fn TVar (v, _) => insert (op =) v | TFree _ => bad_thm - ("Illegal free type variable in rewrite theorem\n" ^ Display.string_of_thm thm))) t []; + ("Illegal free type variable in equation\n" ^ Display.string_of_thm thm))) t []; val lhs_vs = vars_of lhs; val rhs_vs = vars_of rhs; val lhs_tvs = tvars_of lhs; val rhs_tvs = tvars_of rhs; val _ = if null (subtract (op =) lhs_vs rhs_vs) then () - else bad_thm ("Free variables on right hand side of rewrite theorem\n" + else bad_thm ("Free variables on right hand side of equation\n" ^ Display.string_of_thm thm); val _ = if null (subtract (op =) lhs_tvs rhs_tvs) then () - else bad_thm ("Free type variables on right hand side of rewrite theorem\n" + else bad_thm ("Free type variables on right hand side of equation\n" ^ Display.string_of_thm thm) val (head, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; - val (c, ty) = case head of Const c_ty => c_ty | _ => - bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm); + val (c, ty) = case head + of Const (c_ty as (_, ty)) => (AxClass.unoverload_const thy c_ty, ty) + | _ => bad_thm ("Equation not headed by constant\n" ^ Display.string_of_thm thm); fun check _ (Abs _) = bad_thm ("Abstraction on left hand side of equation\n" ^ Display.string_of_thm thm) | check 0 (Var _) = () | check _ (Var _) = bad_thm - ("Variable with application on left hand side of code equation\n" + ("Variable with application on left hand side of equation\n" ^ Display.string_of_thm thm) | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) - | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty - then bad_thm - ("Partially applied constant on left hand side of equation\n" - ^ Display.string_of_thm thm) - else (); + | check n (Const (c_ty as (c, ty))) = if n = (length o fst o strip_type) ty + then if not proper orelse is_constr_pat (AxClass.unoverload_const thy c_ty) + then () + else bad_thm (quote c ^ " is not a constructor, on left hand side of equation\n" + ^ Display.string_of_thm thm) + else bad_thm + ("Partially applied constant " ^ quote c ^ " on left hand side of equation\n" + ^ Display.string_of_thm thm); val _ = map (check 0) args; + val _ = if not proper orelse is_linear thm then () + else bad_thm ("Duplicate variables on left hand side of equation\n" + ^ Display.string_of_thm thm); + val _ = if (is_none o AxClass.class_of_param thy) c + then () + else bad_thm ("Polymorphic constant as head in equation\n" + ^ Display.string_of_thm thm) + val _ = if not (is_constr_head c) + then () + else bad_thm ("Constructor as head in equation\n" + ^ Display.string_of_thm thm) val ty_decl = Sign.the_const_type thy c; val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty) then () else bad_thm ("Type\n" ^ string_of_typ thy ty - ^ "\nof code equation\n" + ^ "\nof equation\n" ^ Display.string_of_thm thm ^ "\nis incompatible with declared function type\n" ^ string_of_typ thy ty_decl) - in thm end; - -fun add_linear thm = - let - val (_, args) = (strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; - val linear = not (has_duplicates (op =) - ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args [])) - in (thm, linear) end; + in (thm, proper) end; -fun assert_pat is_cons thm = - let - val args = (snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm; - val _ = (map o map_aterms) (fn t as Const (c, _) => if is_cons c then t - else bad_thm ("Not a constructor on left hand side of equation: " - ^ quote c ^ ",\n in equation\n" ^ Display.string_of_thm thm) - | t => t) args; - in thm end; - -fun assert_linear is_cons (thm, false) = (thm, false) - | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm)) then (thm, true) - else bad_thm - ("Duplicate variables on left hand side of code equation:\n" - ^ Display.string_of_thm thm); - - -fun mk_eqn thy = add_linear o assert_eqn thy o AxClass.unoverload thy - o LocalDefs.meta_rewrite_rule (ProofContext.init thy); +fun assert_eqn thy is_constr = error_thm (gen_assert_eqn thy is_constr is_constr); val const_typ_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of; -val const_eqn = fst o const_typ_eqn; -fun head_eqn thy thm = let val (c, ty) = const_typ_eqn thm in (c, typscheme thy (c, ty)) end; + +fun typscheme_eqn thy = typscheme thy o const_typ_eqn; + +(*these are permissive wrt. to overloaded constants!*) +fun mk_eqn thy is_constr_head = error_thm (gen_assert_eqn thy is_constr_head (K true)) o + apfst (LocalDefs.meta_rewrite_rule (ProofContext.init thy)); + +fun mk_eqn_liberal thy is_constr_head = Option.map (fn (thm, _) => (thm, is_linear thm)) + o try_thm (gen_assert_eqn thy is_constr_head (K true)) + o rpair false o LocalDefs.meta_rewrite_rule (ProofContext.init thy); + +fun const_eqn thy = AxClass.unoverload_const thy o const_typ_eqn; (* case cerificates *) diff -r 3e69a25b90a2 -r ee45b1c733c1 src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Mon May 11 15:05:17 2009 +0100 +++ b/src/Tools/code/code_thingol.ML Mon May 11 17:08:31 2009 +0200 @@ -591,14 +591,14 @@ translate_term thy algbr funcgr thm t' ##>> fold_map (translate_term thy algbr funcgr thm) ts #>> (fn (t, ts) => t `$$ ts) -and translate_eq thy algbr funcgr (thm, linear) = +and translate_eq thy algbr funcgr (thm, proper) = let val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify o prop_of) thm; in fold_map (translate_term thy algbr funcgr (SOME thm)) args ##>> translate_term thy algbr funcgr (SOME thm) rhs - #>> rpair (thm, linear) + #>> rpair (thm, proper) end and translate_const thy algbr funcgr thm (c, ty) = let diff -r 3e69a25b90a2 -r ee45b1c733c1 src/Tools/code/code_wellsorted.ML --- a/src/Tools/code/code_wellsorted.ML Mon May 11 15:05:17 2009 +0100 +++ b/src/Tools/code/code_wellsorted.ML Mon May 11 17:08:31 2009 +0200 @@ -64,7 +64,7 @@ fun tyscm_rhss_of thy c eqns = let val tyscm = case eqns of [] => Code.default_typscheme thy c - | ((thm, _) :: _) => (snd o Code_Unit.head_eqn thy) thm; + | ((thm, _) :: _) => Code_Unit.typscheme_eqn thy thm; val rhss = consts_of thy eqns; in (tyscm, rhss) end;