487 val T = fastype_of pred |
487 val T = fastype_of pred |
488 val ho_args = ho_args_of_typ T args |
488 val ho_args = ho_args_of_typ T args |
489 fun subst_of (pred', pred) = |
489 fun subst_of (pred', pred) = |
490 let |
490 let |
491 val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty |
491 val subst = Sign.typ_match thy (fastype_of pred', fastype_of pred) Vartab.empty |
|
492 handle TYPE_MATCH => error ("Type mismatch of predicate " ^ fst (dest_Const pred) |
|
493 ^ " (trying to match " ^ Syntax.string_of_typ ctxt (fastype_of pred') |
|
494 ^ " and " ^ Syntax.string_of_typ ctxt (fastype_of pred) ^ ")" |
|
495 ^ " in " ^ Display.string_of_thm ctxt th) |
492 in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end |
496 in map (fn (indexname, (s, T)) => ((indexname, s), T)) (Vartab.dest subst) end |
493 fun instantiate_typ th = |
497 fun instantiate_typ th = |
494 let |
498 let |
495 val (pred', _) = strip_intro_concl th |
499 val (pred', _) = strip_intro_concl th |
496 val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then |
500 val _ = if not (fst (dest_Const pred) = fst (dest_Const pred')) then |