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