equal
deleted
inserted
replaced
587 |> Syntax.read_term_global (Proof_Context.theory_of ctxt) |
587 |> Syntax.read_term_global (Proof_Context.theory_of ctxt) |
588 |> Model_Pattern.adapt_term_to_type ctxt |
588 |> Model_Pattern.adapt_term_to_type ctxt |
589 fun parse_patt_test thy str = (thy, str) |
589 fun parse_patt_test thy str = (thy, str) |
590 |>> Proof_Context.init_global |
590 |>> Proof_Context.init_global |
591 |-> Proof_Context.read_term_pattern |
591 |-> Proof_Context.read_term_pattern |
592 (**)|> typ_a2real; (** )TODO drop*) |
592 |> Model_Pattern.adapt_term_to_type (Proof_Context.init_global thy) |
593 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
593 fun str2term str = parse_patt (ThyC.get_theory "Isac_Knowledge") str |
594 |
594 |
595 |
595 |
596 fun is_atom (Const _) = true |
596 fun is_atom (Const _) = true |
597 | is_atom (Free _) = true |
597 | is_atom (Free _) = true |