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