changeset 56239 | 17df7145a871 |
parent 55437 | 3fd63b92ea3b |
child 59058 | a78612c67ec0 |
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Mar 21 08:13:23 2014 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri Mar 21 10:45:03 2014 +0100 @@ -284,7 +284,7 @@ end val intr_tss = map mk_intros ((funs ~~ preds) ~~ (argss' ~~ rhss)) val (intrs, thy') = thy - |> Sign.add_consts_i + |> Sign.add_consts (map (fn Const (name, T) => (Binding.name (Long_Name.base_name name), T, NoSyn)) dst_preds) |> fold_map Specification.axiom (* FIXME !?!?!?! *)