equal
deleted
inserted
replaced
584 val thy_prefix = Context.theory_name thy ^ Long_Name.separator |
584 val thy_prefix = Context.theory_name thy ^ Long_Name.separator |
585 val global_facts = PureThy.facts_of thy |
585 val global_facts = PureThy.facts_of thy |
586 val local_facts = ProofContext.facts_of ctxt |
586 val local_facts = ProofContext.facts_of ctxt |
587 val named_locals = local_facts |> Facts.dest_static [] |
587 val named_locals = local_facts |> Facts.dest_static [] |
588 val is_chained = member Thm.eq_thm chained_ths |
588 val is_chained = member Thm.eq_thm chained_ths |
589 (* Unnamed, not chained formulas with schematic variables are omitted, |
589 (* Unnamed nonchained formulas with schematic variables are omitted, because |
590 because they are rejected by the backticks (`...`) parser for some |
590 they are rejected by the backticks (`...`) parser for some reason. *) |
591 reason. *) |
|
592 fun is_good_unnamed_local th = |
591 fun is_good_unnamed_local th = |
593 forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals |
592 forall (fn (_, ths) => not (member Thm.eq_thm ths th)) named_locals |
594 andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) |
593 andalso (not (exists_subterm is_Var (prop_of th)) orelse (is_chained th)) |
595 val unnamed_locals = |
594 val unnamed_locals = |
596 local_facts |> Facts.props |> filter is_good_unnamed_local |
595 local_facts |> Facts.props |> filter is_good_unnamed_local |