src/HOL/Tools/typedef_package.ML
changeset 16486 1a12cdb6ee6b
parent 16458 4c6fd0c01d28
child 16645 a152d6b21c31
     1.1 --- a/src/HOL/Tools/typedef_package.ML	Mon Jun 20 22:13:58 2005 +0200
     1.2 +++ b/src/HOL/Tools/typedef_package.ML	Mon Jun 20 22:13:59 2005 +0200
     1.3 @@ -97,7 +97,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 (map (rpair NONE) witn_names) @ witn_thms;
     1.8 +    val thms = PureThy.get_thmss thy (map Name witn_names) @ witn_thms;
     1.9      val tac =
    1.10        witn1_tac THEN
    1.11        TRY (rewrite_goals_tac (List.filter is_def thms)) THEN