396 |
396 |
397 fun flexflex_first_order th = |
397 fun flexflex_first_order th = |
398 (case Thm.tpairs_of th of |
398 (case Thm.tpairs_of th of |
399 [] => th |
399 [] => th |
400 | pairs => |
400 | pairs => |
401 let |
401 let |
402 val thy = Thm.theory_of_thm th |
402 val thy = Thm.theory_of_thm th |
403 val cert = Thm.cterm_of thy |
403 val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) |
404 val certT = Thm.ctyp_of thy |
404 |
405 val (tyenv, tenv) = fold (Pattern.first_order_match thy) pairs (Vartab.empty, Vartab.empty) |
405 fun mkT (v, (S, T)) = apply2 (Thm.ctyp_of thy) (TVar (v, S), T) |
406 |
406 fun mk (v, (T, t)) = apply2 (Thm.cterm_of thy) (Var (v, Envir.subst_type tyenv T), t) |
407 fun mkT (v, (S, T)) = (certT (TVar (v, S)), certT T) |
407 |
408 fun mk (v, (T, t)) = (cert (Var (v, Envir.subst_type tyenv T)), cert t) |
408 val instsT = Vartab.fold (cons o mkT) tyenv [] |
409 |
409 val insts = Vartab.fold (cons o mk) tenv [] |
410 val instsT = Vartab.fold (cons o mkT) tyenv [] |
410 in |
411 val insts = Vartab.fold (cons o mk) tenv [] |
411 Thm.instantiate (instsT, insts) th |
412 in |
412 end |
413 Thm.instantiate (instsT, insts) th |
413 handle THM _ => th) |
414 end |
|
415 handle THM _ => th) |
|
416 |
414 |
417 fun is_metis_literal_genuine (_, (s, _)) = |
415 fun is_metis_literal_genuine (_, (s, _)) = |
418 not (String.isPrefix class_prefix (Metis_Name.toString s)) |
416 not (String.isPrefix class_prefix (Metis_Name.toString s)) |
419 fun is_isabelle_literal_genuine t = |
417 fun is_isabelle_literal_genuine t = |
420 (case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true) |
418 (case t of _ $ (Const (@{const_name Meson.skolem}, _) $ _) => false | _ => true) |