32 \<comment> \<open>TODO pointless to annotate explicit fixes in term\<close> |
32 \<comment> \<open>TODO pointless to annotate explicit fixes in term\<close> |
33 |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) |
33 |> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of) |
34 |> Sledgehammer_Util.simplify_spaces |
34 |> Sledgehammer_Util.simplify_spaces |
35 |> maybe_quote ctxt; |
35 |> maybe_quote ctxt; |
36 |
36 |
37 fun print_isar_skeleton ctxt indent keyword (fixes, assms, concl) = |
37 fun eigen_context_for_statement (fixes, assms, concl) ctxt = |
38 let |
38 let |
39 val (_, ctxt') = Variable.add_fixes (map fst fixes) ctxt; |
39 val (fixes', ctxt') = Variable.add_fixes (map fst fixes) ctxt; |
|
40 val subst_free = AList.lookup (op =) (map fst fixes ~~ fixes') |
|
41 val subst = map_aterms (fn Free (v, T) => Free (the_default v (subst_free v), T) |
|
42 | t => t) |
|
43 val assms' = map subst assms; |
|
44 val concl' = subst concl; |
|
45 in ((fixes, assms', concl'), ctxt') end; |
|
46 |
|
47 fun print_isar_skeleton ctxt indent keyword stmt = |
|
48 let |
|
49 val ((fixes, assms, concl), ctxt') = eigen_context_for_statement stmt ctxt; |
40 val prefix = replicate_string indent " "; |
50 val prefix = replicate_string indent " "; |
41 \<comment> \<open>TODO consider pre-existing indentation -- how?\<close> |
51 \<comment> \<open>TODO consider pre-existing indentation -- how?\<close> |
42 val prefix_sep = "\n" ^ prefix ^ " and "; |
52 val prefix_sep = "\n" ^ prefix ^ " and "; |
43 val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl; |
53 val show_s = prefix ^ keyword ^ " " ^ print_term ctxt' concl; |
44 val if_s = if null assms then NONE |
54 val if_s = if null assms then NONE |