1135   case trm of

  1135   case trm of

  1136     Abs (x, T, t) =>

  1136     Abs (x, T, t) =>

  1137        let 

  1137        let 

  1138           val ty1 = fastype_of trm

  1138           val ty1 = fastype_of trm

  1139        in

  1139        in

  1141        end

  1141        end

  1142   | Const (@{const_name "All"}, U) $ t =>

  1142   | Const (@{const_name "All"}, U) $ t =>

  1143        let 

  1143        let 

  1144           val ty1 = fastype_of t

  1144           val ty1 = fastype_of t

  1145           val ty2 = domain_type ty1

  1145           val ty2 = domain_type ty1

  1151           val ty1 = fastype_of t

  1151           val ty1 = fastype_of t

  1152           val ty2 = domain_type ty1

  1152           val ty2 = domain_type ty1

  1153        in

  1153        in

  1154          (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    

  1154          (mk_bex ty1) $ (mk_resp ty2 $ rel) $ (apply_subt (my_reg rel) t)    

  1155        end

  1155        end

  1156   | _ => trm

  1157   | _ => trm

  1157 *}

  1158 *}

  1158 

  1159 

  1159 ML {*  

  1160 ML {*  

  1160   cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});

  1161   cterm_of @{theory} (regularise @{term "\<lambda>x::trm. x"} @{typ "trm"} @{term "RR"} @{context});