- let proof,gl = Tacticals.then_
- ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
- ~continuation:(PrimitiveTactics.intros_tac ~name:fhyp)
- ~status:(s_proof,s_goal) in
+ let proof,gl =
+ Tacticals.then_
+ ~start:(PrimitiveTactics.apply_tac ~term:!th_to_appl)
+ ~continuation:PrimitiveTactics.intros_tac
+ ~status:(s_proof,s_goal) in