src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 60251 98754695b421
parent 59936 b8ffc3dc9e24
child 60279 351536745704
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 03 20:21:25 2015 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Sun May 03 18:14:11 2015 +0200
     1.3 @@ -751,7 +751,7 @@
     1.4  
     1.5          fun prove_split selss goal =
     1.6            Goal.prove_sorry lthy [] [] goal (fn _ =>
     1.7 -            mk_split_tac lthy uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
     1.8 +            mk_split_tac lthy ms uexhaust_thm case_thms selss inject_thmss distinct_thmsss)
     1.9            |> singleton (Proof_Context.export names_lthy lthy)
    1.10            |> Thm.close_derivation;
    1.11