src/HOL/Tools/typedef_package.ML
changeset 15457 1fbd4aba46e3
parent 15265 a1547232fedd
child 15531 08c8dad8e399
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Jan 24 17:56:18 2005 +0100
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Jan 24 17:59:48 2005 +0100
     1.3 @@ -101,7 +101,7 @@
     1.4  fun prove_nonempty thy cset goal (witn1_tac, witn_names, witn_thms, witn2_tac) =
     1.5    let
     1.6      val is_def = Logic.is_equals o #prop o Thm.rep_thm;
     1.7 -    val thms = PureThy.get_thmss thy witn_names @ witn_thms;
     1.8 +    val thms = PureThy.get_thmss thy (map (rpair None) witn_names) @ witn_thms;
     1.9      val tac =
    1.10        witn1_tac THEN
    1.11        TRY (rewrite_goals_tac (filter is_def thms)) THEN