equal
deleted
inserted
replaced
43 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
43 fun nth_conj n (_, r) = nth (HOLogic.dest_conj r) n; |
44 |
44 |
45 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
45 fun style_lhs_rhs proj = Scan.succeed (fn ctxt => fn t => |
46 let |
46 let |
47 val concl = |
47 val concl = |
48 Object_Logic.drop_judgment (ProofContext.theory_of ctxt) (Logic.strip_imp_concl t) |
48 Object_Logic.drop_judgment (Proof_Context.theory_of ctxt) (Logic.strip_imp_concl t) |
49 in |
49 in |
50 case concl of (_ $ l $ r) => proj (l, r) |
50 case concl of (_ $ l $ r) => proj (l, r) |
51 | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl) |
51 | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl) |
52 end); |
52 end); |
53 *} |
53 *} |