src/HOL/Tools/typedef_package.ML
changeset 10697 ec197510165a
parent 10675 0b40c19f09f3
child 11426 f280d4b29a2c
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Dec 18 16:45:17 2000 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Tue Dec 19 13:06:49 2000 +0100
     1.3 @@ -154,9 +154,9 @@
     1.4      val typedef_prop = HOLogic.mk_Trueprop (typedefC $ RepC $ AbsC $ set');
     1.5  
     1.6      (*theory extender*)
     1.7 -    fun do_typedef theory =
     1.8 +    fun do_typedef super_theory theory =
     1.9        theory
    1.10 -      |> Theory.assert_super thy
    1.11 +      |> Theory.assert_super super_theory
    1.12        |> add_typedecls [(t, vs, mx)]
    1.13        |> Theory.add_consts_i
    1.14         ((if no_def then [] else [(name, setT, NoSyn)]) @
    1.15 @@ -219,7 +219,7 @@
    1.16    let
    1.17      val (cset, _, do_typedef) = prepare_typedef prep_term no_def name typ set thy;
    1.18      val result = prove_nonempty thy cset (names, thms, tac);
    1.19 -  in check_nonempty cset result; thy |> do_typedef |> #1 end;
    1.20 +  in check_nonempty cset result; thy |> do_typedef thy |> #1 end;
    1.21  
    1.22  val add_typedef = gen_add_typedef read_term false;
    1.23  val add_typedef_i = gen_add_typedef cert_term false;
    1.24 @@ -236,9 +236,10 @@
    1.25      val (cset, cset_pat, do_typedef) = prepare_typedef prep_term false name typ set thy;
    1.26      val goal = Thm.term_of (goal_nonempty true cset);
    1.27      val goal_pat = Thm.term_of (goal_nonempty true cset_pat);
    1.28 +    val test_thy = Theory.copy thy;
    1.29    in
    1.30 -    thy
    1.31 -    |> IsarThy.theorem_i ((("", [typedef_attribute cset do_typedef]),
    1.32 +    test_thy |> do_typedef test_thy;  (*preview errors!*)
    1.33 +    thy |> IsarThy.theorem_i ((("", [typedef_attribute cset (do_typedef thy)]),
    1.34        (goal, ([goal_pat], []))), comment) int
    1.35    end;
    1.36