1072   end

  1072   end

  1073 *}

  1073 *}

  1074 

  1074 

  1075 

  1075 

  1076 ML {*

  1076 ML {*

  1078   val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))

  1079   val _ = tracing ("raw theorem:\n" ^ Syntax.string_of_term lthy (prop_of rthm))

  1079 

  1080 

  1080   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

  1081   val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data lthy qty;

  1081   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

  1082   val (trans2, reps_same, absrep, quot) = lookup_quot_thms lthy qty_name;

  1082   val consts = lookup_quot_consts defs;

  1083   val consts = lookup_quot_consts defs;

  1131 in

  1132 in

  1132   Thm.varifyT t_rv

  1133   Thm.varifyT t_rv

  1133 end

  1134 end

  1134 *}

  1135 *}

  1135 

  1136 

  1137 ML {*

  1137 ML {*

  1138 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =

  1138 fun lift_thm_note qty qty_name rsp_thms defs thm name lthy =

  1139   let

  1139   let

  1140     val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;

  1140     val lifted_thm = lift_thm lthy qty qty_name rsp_thms defs thm;

  1141     val (_, lthy2) = note (name, lifted_thm) lthy;

  1141     val (_, lthy2) = note (name, lifted_thm) lthy;

  1142   in

  1142   in

  1143     lthy2

  1143     lthy2

  1144   end

  1144   end

  1145 *}

  1145 *}

  1146 

  1146 

  1149 end

  1159 end