src/Tools/IsaPlanner/isand.ML
changeset 52467 24c6ddb48cb8
parent 52246 54c0d4128b30
child 59582 0fbed69ff081
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Thu Jun 27 12:34:58 2013 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Thu Jun 27 17:06:22 2013 +0200
     1.3 @@ -50,7 +50,7 @@
     1.4      val solth' = solth
     1.5        |> Drule.implies_intr_list hcprems
     1.6        |> Drule.forall_intr_list cfvs;
     1.7 -  in Drule.compose_single (solth', i, gth) end;
     1.8 +  in Drule.compose (solth', i, gth) end;
     1.9  
    1.10  fun variant_names ctxt ts xs =
    1.11    let