src/HOL/Tools/inductive_set.ML
changeset 33671 4b0f2599ed48
parent 33670 02b7738aef6a
child 33766 c679f05600cd
     1.1 --- a/src/HOL/Tools/inductive_set.ML	Fri Nov 13 20:41:29 2009 +0100
     1.2 +++ b/src/HOL/Tools/inductive_set.ML	Fri Nov 13 21:11:15 2009 +0100
     1.3 @@ -484,13 +484,13 @@
     1.4  
     1.5      (* define inductive sets using previously defined predicates *)
     1.6      val (defs, lthy2) = lthy1
     1.7 -      |> LocalTheory.conceal  (* FIXME ?? *)
     1.8 -      |> fold_map (LocalTheory.define "")
     1.9 +      |> Local_Theory.conceal  (* FIXME ?? *)
    1.10 +      |> fold_map (Local_Theory.define "")
    1.11          (map (fn ((c_syn, (fs, U, _)), p) => (c_syn, (Attrib.empty_binding,
    1.12             fold_rev lambda params (HOLogic.Collect_const U $
    1.13               HOLogic.mk_psplits fs U HOLogic.boolT (list_comb (p, params3))))))
    1.14             (cnames_syn ~~ cs_info ~~ preds))
    1.15 -      ||> LocalTheory.restore_naming lthy1;
    1.16 +      ||> Local_Theory.restore_naming lthy1;
    1.17  
    1.18      (* prove theorems for converting predicate to set notation *)
    1.19      val lthy3 = fold
    1.20 @@ -505,7 +505,7 @@
    1.21              (K (REPEAT (rtac ext 1) THEN simp_tac (HOL_basic_ss addsimps
    1.22                [def, mem_Collect_eq, split_conv]) 1))
    1.23          in
    1.24 -          lthy |> LocalTheory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    1.25 +          lthy |> Local_Theory.note ((Binding.name (s ^ "p_" ^ s ^ "_eq"),
    1.26              [Attrib.internal (K pred_set_conv_att)]),
    1.27                [conv_thm]) |> snd
    1.28          end) (preds ~~ cs ~~ cs_info ~~ defs) lthy2;
    1.29 @@ -515,7 +515,7 @@
    1.30        if Binding.is_empty alt_name then
    1.31          Binding.name (space_implode "_" (map (Binding.name_of o fst) cnames_syn))
    1.32        else alt_name;
    1.33 -    val cnames = map (LocalTheory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
    1.34 +    val cnames = map (Local_Theory.full_name lthy3 o #1) cnames_syn;  (* FIXME *)
    1.35      val (intr_names, intr_atts) = split_list (map fst intros);
    1.36      val raw_induct' = to_set [] (Context.Proof lthy3) raw_induct;
    1.37      val (intrs', elims', induct, lthy4) =