src/HOL/Tools/inductive_codegen.ML
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18928 042608ffa2ec
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Jan 20 04:53:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sat Jan 21 23:02:14 2006 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  
     1.5  signature INDUCTIVE_CODEGEN =
     1.6  sig
     1.7 -  val add : string option -> theory attribute
     1.8 +  val add : string option -> attribute
     1.9    val setup : theory -> theory
    1.10  end;
    1.11  
    1.12 @@ -45,7 +45,7 @@
    1.13  
    1.14  fun add_node (g, x) = Graph.new_node (x, ()) g handle Graph.DUP _ => g;
    1.15  
    1.16 -fun add optmod (p as (thy, thm)) =
    1.17 +fun add optmod = Thm.declaration_attribute (fn thm => Context.map_theory (fn thy =>
    1.18    let
    1.19      val {intros, graph, eqns} = CodegenData.get thy;
    1.20      fun thyname_of s = (case optmod of
    1.21 @@ -54,22 +54,22 @@
    1.22        _ $ (Const ("op :", _) $ _ $ t) => (case head_of t of
    1.23          Const (s, _) =>
    1.24            let val cs = foldr add_term_consts [] (prems_of thm)
    1.25 -          in (CodegenData.put
    1.26 +          in CodegenData.put
    1.27              {intros = intros |>
    1.28               Symtab.update (s, Symtab.lookup_multi intros s @ [(thm, thyname_of s)]),
    1.29               graph = foldr (uncurry (Graph.add_edge o pair s))
    1.30                 (Library.foldl add_node (graph, s :: cs)) cs,
    1.31 -             eqns = eqns} thy, thm)
    1.32 +             eqns = eqns} thy
    1.33            end
    1.34 -      | _ => (warn thm; p))
    1.35 +      | _ => (warn thm; thy))
    1.36      | _ $ (Const ("op =", _) $ t $ _) => (case head_of t of
    1.37          Const (s, _) =>
    1.38 -          (CodegenData.put {intros = intros, graph = graph,
    1.39 +          CodegenData.put {intros = intros, graph = graph,
    1.40               eqns = eqns |> Symtab.update
    1.41 -               (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy, thm)
    1.42 -      | _ => (warn thm; p))
    1.43 -    | _ => (warn thm; p))
    1.44 -  end;
    1.45 +               (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy
    1.46 +      | _ => (warn thm; thy))
    1.47 +    | _ => (warn thm; thy))
    1.48 +  end));
    1.49  
    1.50  fun get_clauses thy s =
    1.51    let val {intros, graph, ...} = CodegenData.get thy