38 fun err msg ts = |
38 fun err msg ts = |
39 error (cat_lines (msg :: map (Sign.string_of_term sign) ts)); |
39 error (cat_lines (msg :: map (Sign.string_of_term sign) ts)); |
40 |
40 |
41 val ctxt = |
41 val ctxt = |
42 ProofContext.init thy |> ProofContext.add_fixes |
42 ProofContext.init thy |> ProofContext.add_fixes |
43 (flat (map (fn (As, T) => map (fn A => (A, T, NONE)) As) structs)); |
43 (List.concat (map (fn (As, T) => map (fn A => (A, T, NONE)) As) structs)); |
44 val (ctxt', d, mx) = |
44 val (ctxt', d, mx) = |
45 (case decl of NONE => (ctxt, NONE, Syntax.NoSyn) | SOME (x, raw_T, mx) => |
45 (case decl of NONE => (ctxt, NONE, Syntax.NoSyn) | SOME (x, raw_T, mx) => |
46 let |
46 let |
47 val x' = Syntax.const_name x mx and mx' = Syntax.fix_mixfix x mx; |
47 val x' = Syntax.const_name x mx and mx' = Syntax.fix_mixfix x mx; |
48 val T = apsome (prep_typ ctxt) raw_T; |
48 val T = Option.map (prep_typ ctxt) raw_T; |
49 in (ProofContext.add_fixes_liberal [(x', T, SOME mx')] ctxt, SOME x', mx') end); |
49 in (ProofContext.add_fixes_liberal [(x', T, SOME mx')] ctxt, SOME x', mx') end); |
50 |
50 |
51 val prop = prep_term ctxt' raw_prop; |
51 val prop = prep_term ctxt' raw_prop; |
52 val concl = Logic.strip_imp_concl prop; |
52 val concl = Logic.strip_imp_concl prop; |
53 val (lhs, _) = Logic.dest_equals concl handle TERM _ => |
53 val (lhs, _) = Logic.dest_equals concl handle TERM _ => |