src/Pure/deriv.ML
changeset 2672 85d7e800d754
parent 2042 33b4c1624e26
child 6085 3d8dcb09dbfb
equal deleted inserted replaced
2671:510d94c71dda 2672:85d7e800d754
    36               Join(Assumption arg,[]) :: rev_deriv der
    36               Join(Assumption arg,[]) :: rev_deriv der
    37   | rev_deriv (Join (Bicompose arg, [rder, sder])) =
    37   | rev_deriv (Join (Bicompose arg, [rder, sder])) =
    38 	Join (Bicompose arg, linear rder) :: rev_deriv sder
    38 	Join (Bicompose arg, linear rder) :: rev_deriv sder
    39   | rev_deriv (Join (_, [der]))	= rev_deriv der
    39   | rev_deriv (Join (_, [der]))	= rev_deriv der
    40   | rev_deriv (Join (rl, der::ders)) =	(*catch-all case; doubtful?*)
    40   | rev_deriv (Join (rl, der::ders)) =	(*catch-all case; doubtful?*)
    41         Join(rl, flat (map linear ders)) :: rev_deriv der
    41         Join(rl, List.concat (map linear ders)) :: rev_deriv der
    42 and linear der 	= rev (rev_deriv der);
    42 and linear der 	= rev (rev_deriv der);
    43 
    43 
    44 
    44 
    45 (*** Conversion of object-level proof trees ***)
    45 (*** Conversion of object-level proof trees ***)
    46 
    46