src/HOL/Tools/typedef_package.ML
changeset 6935 a3f3f4128cab
parent 6729 b6e167580a32
child 7152 44d46a112127
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Thu Jul 08 18:35:44 1999 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Thu Jul 08 18:36:09 1999 +0200
     1.3 @@ -195,7 +195,7 @@
     1.4      val goal = Thm.term_of (goal_nonempty cset);
     1.5    in
     1.6      thy
     1.7 -    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, [])), comment) int
     1.8 +    |> IsarThy.theorem_i (("", [typedef_attribute cset do_typedef], (goal, ([], []))), comment) int
     1.9    end;
    1.10  
    1.11  val typedef_proof = gen_typedef_proof read_term;