1theory Setup
2imports Complex_Main "HOL-Library.Multiset" "HOL-Library.Lattice_Syntax"
3begin
4
5ML_file "../antiquote_setup.ML"
6ML_file "../more_antiquote.ML"
7
8attribute_setup all =
9  \<open>Scan.succeed (Thm.rule_attribute [] (K Drule.forall_intr_vars))\<close>
10  "quantified schematic vars"
11
12setup \<open>Config.put_global Printer.show_type_emphasis false\<close>
13
14setup \<open>
15let
16  fun strip_all t =
17    if Logic.is_all t
18    then
19      case snd (dest_comb t) of Abs (w, T, t') =>
20        strip_all t' |>> cons (w, T)
21    else ([], t);
22  fun frugal (w, T as TFree (v, sort)) visited =
23        if member (op =) visited v
24        then ((w, dummyT), visited) else ((w, T), v :: visited)
25    | frugal (w, T) visited = ((w, dummyT), visited);
26  fun frugal_sorts t =
27    let
28      val (vTs, body) = strip_all t
29      val (vTs', _) = fold_map frugal vTs [];
30    in Logic.list_all (vTs', map_types (K dummyT) body) end;
31in
32  Term_Style.setup @{binding frugal_sorts}
33    (Scan.succeed (K frugal_sorts))
34end
35\<close>
36
37declare [[show_sorts]]
38
39end
40