src/HOL/Tools/function_package/fundef_package.ML
changeset 26129 14f6dbb195c4
parent 25222 78943ac46f6d
child 26171 5426a823455c
     1.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Feb 25 16:31:15 2008 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Feb 25 16:31:17 2008 +0100
     1.3 @@ -90,7 +90,7 @@
     1.4      end
     1.5  
     1.6  
     1.7 -fun gen_add_fundef prep fixspec eqnss config flags lthy =
     1.8 +fun gen_add_fundef set_group prep fixspec eqnss config flags lthy =
     1.9      let
    1.10        val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
    1.11        val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    1.12 @@ -103,6 +103,7 @@
    1.13        val afterqed = fundef_afterqed config fixes post defname cont sort_cont cnames
    1.14      in
    1.15        lthy
    1.16 +        |> set_group ? LocalTheory.set_group (serial_string ())
    1.17          |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
    1.18          |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
    1.19      end
    1.20 @@ -150,8 +151,8 @@
    1.21      end
    1.22  
    1.23  
    1.24 -val add_fundef = gen_add_fundef Specification.read_specification
    1.25 -val add_fundef_i = gen_add_fundef Specification.check_specification
    1.26 +val add_fundef = gen_add_fundef true Specification.read_specification
    1.27 +val add_fundef_i = gen_add_fundef false Specification.check_specification
    1.28  
    1.29  
    1.30  (* Datatype hook to declare datatype congs as "fundef_congs" *)