src/HOL/Tools/inductive.ML
changeset 39248 4a3747517552
parent 38864 4abe644fcea5
child 40316 665862241968
     1.1 --- a/src/HOL/Tools/inductive.ML	Wed Sep 08 19:23:23 2010 +0200
     1.2 +++ b/src/HOL/Tools/inductive.ML	Thu Sep 09 09:11:13 2010 +0200
     1.3 @@ -789,14 +789,12 @@
     1.4              val xs = map Free (Variable.variant_frees lthy intr_ts
     1.5                (mk_names "x" (length Ts) ~~ Ts))
     1.6            in
     1.7 -            (name_mx, (Attrib.empty_binding, fold_rev lambda (params @ xs)
     1.8 +            (name_mx, (apfst Binding.conceal Attrib.empty_binding, fold_rev lambda (params @ xs)
     1.9                (list_comb (rec_const, params @ make_bool_args' bs i @
    1.10                  make_args argTs (xs ~~ Ts)))))
    1.11            end) (cnames_syn ~~ cs);
    1.12      val (consts_defs, lthy'') = lthy'
    1.13 -      |> Local_Theory.conceal
    1.14 -      |> fold_map Local_Theory.define specs
    1.15 -      ||> Local_Theory.restore_naming lthy';
    1.16 +      |> fold_map Local_Theory.define specs;
    1.17      val preds = (case cs of [_] => [rec_const] | _ => map #1 consts_defs);
    1.18  
    1.19      val (_, lthy''') = Variable.add_fixes (map (fst o dest_Free) params) lthy'';