src/HOL/Tools/inductive_realizer.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18929 d81435108688
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -467,7 +467,7 @@
     1.4      Library.foldl (add_ind_realizer rsets intrs induct raw_induct elims) (thy, vss)
     1.5    end
     1.6  
     1.7 -fun rlz_attrib arg (thy, thm) =
     1.8 +fun rlz_attrib arg = Thm.declaration_attribute (fn thm => Context.map_theory
     1.9    let
    1.10      fun err () = error "ind_realizer: bad rule";
    1.11      val sets =
    1.12 @@ -476,21 +476,19 @@
    1.13           | xs => map (set_of o fst o HOLogic.dest_imp) xs)
    1.14           handle TERM _ => err () | Empty => err ();
    1.15    in 
    1.16 -    (add_ind_realizers (hd sets) (case arg of
    1.17 +    add_ind_realizers (hd sets)
    1.18 +      (case arg of
    1.19          NONE => sets | SOME NONE => []
    1.20        | SOME (SOME sets') => sets \\ sets')
    1.21 -      thy, thm)
    1.22 -  end;
    1.23 +  end);
    1.24  
    1.25 -val rlz_attrib_global = Attrib.syntax
    1.26 +val ind_realizer = Attrib.syntax
    1.27   ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
    1.28      Scan.option (Scan.lift (Args.colon) |--
    1.29 -      Scan.repeat1 Args.global_const))) >> rlz_attrib);
    1.30 +      Scan.repeat1 Args.const))) >> rlz_attrib);
    1.31  
    1.32  val setup =
    1.33 -  Attrib.add_attributes [("ind_realizer",
    1.34 -    (rlz_attrib_global, K Attrib.undef_local_attribute),
    1.35 -    "add realizers for inductive set")];
    1.36 +  Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
    1.37  
    1.38  end;
    1.39