src/HOL/Import/proof_kernel.ML
changeset 17335 7cff05c90a0e
parent 17328 7bbfb79eda96
child 17379 85109eec887b
equal deleted inserted replaced
17334:6e5815f4d770 17335:7cff05c90a0e
  1327     let
  1327     let
  1328 	val _ = message "INST:"
  1328 	val _ = message "INST:"
  1329 	val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
  1329 	val _ = if_debug (app (fn (x,y) => (prin x; prin y))) sigma
  1330 	val _ = if_debug pth hth
  1330 	val _ = if_debug pth hth
  1331 	val sg = sign_of thy
  1331 	val sg = sign_of thy
  1332 	val (sdom,srng) = ListPair.unzip sigma
  1332 	val (sdom,srng) = ListPair.unzip (rev sigma)
  1333 	val th = hthm2thm hth
  1333 	val th = hthm2thm hth
  1334 	val th1 = mk_INST (map (cterm_of sg) sdom) (map (cterm_of sg) srng) th
  1334 	val th1 = mk_INST (map (cterm_of sg) sdom) (map (cterm_of sg) srng) th
  1335 	val res = HOLThm([],th1)
  1335 	val res = HOLThm([],th1)
  1336 	val _ = message "RESULT:"
  1336 	val _ = message "RESULT:"
  1337 	val _ = if_debug pth res
  1337 	val _ = if_debug pth res