LocalTheory.set_group for user command;
authorwenzelm
Mon Feb 25 16:31:17 2008 +0100 (2008-02-25)
changeset 2612914f6dbb195c4
parent 26128 fe2d24c26e0c
child 26130 03a7cfed5e9e
LocalTheory.set_group for user command;
src/HOL/Tools/function_package/fundef_datatype.ML
src/HOL/Tools/function_package/fundef_package.ML
src/HOL/Tools/function_package/inductive_wrap.ML
src/HOL/Tools/primrec_package.ML
     1.1 --- a/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Feb 25 16:31:15 2008 +0100
     1.2 +++ b/src/HOL/Tools/function_package/fundef_datatype.ML	Mon Feb 25 16:31:17 2008 +0100
     1.3 @@ -305,6 +305,7 @@
     1.4  
     1.5  fun fun_cmd config fixes statements flags lthy =
     1.6      lthy
     1.7 +      |> LocalTheory.set_group (serial_string ())
     1.8        |> FundefPackage.add_fundef fixes statements config flags
     1.9        |> by_pat_completeness_simp
    1.10        |> LocalTheory.reinit
     2.1 --- a/src/HOL/Tools/function_package/fundef_package.ML	Mon Feb 25 16:31:15 2008 +0100
     2.2 +++ b/src/HOL/Tools/function_package/fundef_package.ML	Mon Feb 25 16:31:17 2008 +0100
     2.3 @@ -90,7 +90,7 @@
     2.4      end
     2.5  
     2.6  
     2.7 -fun gen_add_fundef prep fixspec eqnss config flags lthy =
     2.8 +fun gen_add_fundef set_group prep fixspec eqnss config flags lthy =
     2.9      let
    2.10        val ((fixes, spec), ctxt') = prep fixspec (map (fn (n_a, eq) => [(n_a, [eq])]) eqnss) lthy
    2.11        val (eqs, post, sort_cont, cnames) = FundefCommon.get_preproc lthy config flags ctxt' fixes spec
    2.12 @@ -103,6 +103,7 @@
    2.13        val afterqed = fundef_afterqed config fixes post defname cont sort_cont cnames
    2.14      in
    2.15        lthy
    2.16 +        |> set_group ? LocalTheory.set_group (serial_string ())
    2.17          |> Proof.theorem_i NONE afterqed [[(Logic.unprotect (concl_of goalstate), [])]]
    2.18          |> Proof.refine (Method.primitive_text (fn _ => goalstate)) |> Seq.hd
    2.19      end
    2.20 @@ -150,8 +151,8 @@
    2.21      end
    2.22  
    2.23  
    2.24 -val add_fundef = gen_add_fundef Specification.read_specification
    2.25 -val add_fundef_i = gen_add_fundef Specification.check_specification
    2.26 +val add_fundef = gen_add_fundef true Specification.read_specification
    2.27 +val add_fundef_i = gen_add_fundef false Specification.check_specification
    2.28  
    2.29  
    2.30  (* Datatype hook to declare datatype congs as "fundef_congs" *)
     3.1 --- a/src/HOL/Tools/function_package/inductive_wrap.ML	Mon Feb 25 16:31:15 2008 +0100
     3.2 +++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Mon Feb 25 16:31:17 2008 +0100
     3.3 @@ -43,7 +43,6 @@
     3.4            InductivePackage.add_inductive_i
     3.5              {verbose = ! Toplevel.debug,
     3.6                kind = Thm.internalK,
     3.7 -              group = serial_string (),   (* FIXME pass proper group (!?) *)
     3.8                alt_name = "",
     3.9                coind = false,
    3.10                no_elim = false,
     4.1 --- a/src/HOL/Tools/primrec_package.ML	Mon Feb 25 16:31:15 2008 +0100
     4.2 +++ b/src/HOL/Tools/primrec_package.ML	Mon Feb 25 16:31:17 2008 +0100
     4.3 @@ -221,7 +221,7 @@
     4.4      val _ = message ("Proving equations for primrec function(s) " ^ commas_quote names);
     4.5    in map (fn (name_attr, t) => (name_attr, [Goal.prove ctxt [] [] t tac])) end;
     4.6  
     4.7 -fun gen_primrec prep_spec raw_fixes raw_spec lthy =
     4.8 +fun gen_primrec set_group prep_spec raw_fixes raw_spec lthy =
     4.9    let
    4.10      val (fixes, spec) = prepare_spec prep_spec lthy raw_fixes raw_spec;
    4.11      val eqns = fold_rev (process_eqn (fn v => Variable.is_fixed lthy v
    4.12 @@ -248,6 +248,7 @@
    4.13        [Simplifier.simp_add, RecfunCodegen.add NONE];
    4.14    in
    4.15      lthy
    4.16 +    |> set_group ? LocalTheory.set_group (serial_string ())
    4.17      |> fold_map (LocalTheory.define Thm.definitionK o make_def lthy fixes fs) defs
    4.18      |-> (fn defs => `(fn ctxt => prove_spec ctxt names1 rec_rewrites defs spec))
    4.19      |-> (fn simps => fold_map (LocalTheory.note Thm.theoremK) simps)
    4.20 @@ -261,8 +262,8 @@
    4.21  
    4.22  in
    4.23  
    4.24 -val add_primrec = gen_primrec Specification.check_specification;
    4.25 -val add_primrec_cmd = gen_primrec Specification.read_specification;
    4.26 +val add_primrec = gen_primrec false Specification.check_specification;
    4.27 +val add_primrec_cmd = gen_primrec true Specification.read_specification;
    4.28  
    4.29  end;
    4.30