1178 let

  1178 let

  1179   val rtrm_str = quote (Syntax.string_of_term lthy rtrm) 

  1179   val rtrm_str = quote (Syntax.string_of_term lthy rtrm) 

  1180   val qtrm_str = quote (Syntax.string_of_term lthy qtrm)

  1180   val qtrm_str = quote (Syntax.string_of_term lthy qtrm)

  1181   val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]

  1181   val msg = ["The quotient theorem", qtrm_str, "and lifted theorem", rtrm_str, "do not match."]

  1182 in

  1182 in

  1184 end 

  1184 end 

  1185 *}

  1185 *}

  1186 

  1186 

  1187 ML {*

  1187 ML {*

  1188 (* - applies f to the subterm of an abstraction,   *)

  1188 (* - applies f to the subterm of an abstraction,   *)