src/Tools/IsaPlanner/isand.ML
changeset 31945 d5f186aa0bed
parent 30190 479806475f3c
child 35845 e5980f0ad025
     1.1 --- a/src/Tools/IsaPlanner/isand.ML	Mon Jul 06 20:36:38 2009 +0200
     1.2 +++ b/src/Tools/IsaPlanner/isand.ML	Mon Jul 06 21:24:30 2009 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4  fun solve_with sol th = 
     1.5      let fun solvei 0 = Seq.empty
     1.6            | solvei i = 
     1.7 -            Seq.append (bicompose false (false,sol,0) i th) (solvei (i - 1))
     1.8 +            Seq.append (Thm.bicompose false (false,sol,0) i th) (solvei (i - 1))
     1.9      in
    1.10        solvei (Thm.nprems_of th)
    1.11      end;
    1.12 @@ -337,7 +337,7 @@
    1.13  
    1.14        val newth' = Drule.implies_intr_list sgallcts allified_newth
    1.15      in
    1.16 -      bicompose false (false, newth', (length sgallcts)) i gth
    1.17 +      Thm.bicompose false (false, newth', (length sgallcts)) i gth
    1.18      end;
    1.19  
    1.20  (*