src/HOL/Tools/inductive_set.ML
changeset 33278 ba9f52f56356
parent 33049 c38f02fdf35d
child 33368 b1cf34f1855c
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Wed Oct 28 16:25:26 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Wed Oct 28 16:25:27 2009 +0100
     1.3 @@ -407,7 +407,7 @@
     1.4  fun add_ind_set_def
     1.5      {quiet_mode, verbose, kind, alt_name, coind, no_elim, no_ind, skip_mono, fork_mono}
     1.6      cs intros monos params cnames_syn ctxt =
     1.7 -  let
     1.8 +  let (* FIXME proper naming convention: lthy *)
     1.9      val thy = ProofContext.theory_of ctxt;
    1.10      val {set_arities, pred_arities, to_pred_simps, ...} =
    1.11        PredSetConvData.get (Context.Proof ctxt);
    1.12 @@ -419,7 +419,8 @@
    1.13      val new_arities = filter_out
    1.14        (fn (x as Free (_, T), _) => x mem params andalso length (binder_types T) > 1
    1.15          | _ => false) (fold (snd #> infer) intros []);
    1.16 -    val params' = map (fn x => (case AList.lookup op = new_arities x of
    1.17 +    val params' = map (fn x =>
    1.18 +      (case AList.lookup op = new_arities x of
    1.19          SOME fs =>
    1.20            let
    1.21              val T = HOLogic.dest_setT (fastype_of x);
    1.22 @@ -482,11 +483,14 @@
    1.23          cs' intros' monos' params1 cnames_syn' ctxt;
    1.24  
    1.25      (* define inductive sets using previously defined predicates *)
    1.26 -    val (defs, ctxt2) = fold_map (LocalTheory.define Thm.internalK)
    1.27 -      (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    1.28 -         fold_rev lambda params (HOLogic.Collect_const U $
    1.29 -           HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
    1.30 -         (cnames_syn ~~ cs_info ~~ preds)) ctxt1;
    1.31 +    val (defs, ctxt2) = ctxt1
    1.32 +      |> LocalTheory.conceal  (* FIXME ?? *)
    1.33 +      |> fold_map (LocalTheory.define Thm.internalK)
    1.34 +        (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    1.35 +           fold_rev lambda params (HOLogic.Collect_const U $
    1.36 +             HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
    1.37 +           (cnames_syn ~~ cs_info ~~ preds))
    1.38 +      ||> LocalTheory.restore_naming ctxt1;
    1.39  
    1.40      (* prove theorems for converting predicate to set notation *)
    1.41      val ctxt3 = fold