src/Pure/Thy/term_style.ML
changeset 41685 e29ea98a76ce
parent 36950 75b8f26f2f07
child 41686 d8efc2490b8e
     1.1 --- a/src/Pure/Thy/term_style.ML	Mon Jan 31 23:53:07 2011 +0100
     1.2 +++ b/src/Pure/Thy/term_style.ML	Tue Feb 01 21:09:52 2011 +0100
     1.3 @@ -94,11 +94,30 @@
     1.4        " in propositon: " ^ Syntax.string_of_term ctxt t)
     1.5    end);
     1.6  
     1.7 +fun isub_symbols (d :: s :: ss) =
     1.8 +      if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
     1.9 +      then d :: "\\<^isub>" :: isub_symbols (s :: ss)
    1.10 +      else d :: s :: ss
    1.11 +  | isub_symbols cs = cs;
    1.12 +
    1.13 +val isub_name = implode o rev o isub_symbols o rev o Symbol.explode;
    1.14 +
    1.15 +fun isub_term (Free (n, T)) = Free (isub_name n, T)
    1.16 +  | isub_term (Var ((n, idx), T)) =
    1.17 +      if idx <> 0 then Var ((isub_name (n ^ string_of_int idx), 0), T)
    1.18 +      else Var ((isub_name n, 0), T)
    1.19 +  | isub_term (t $ u) = isub_term t $ isub_term u
    1.20 +  | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
    1.21 +  | isub_term t = t;
    1.22 +
    1.23 +val style_isub = Scan.succeed (K isub_term);
    1.24 +
    1.25  val _ = Context.>> (Context.map_theory
    1.26   (setup "lhs" (style_lhs_rhs fst) #>
    1.27    setup "rhs" (style_lhs_rhs snd) #>
    1.28    setup "prem" style_prem #>
    1.29    setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
    1.30 +  setup "isub" style_isub #>
    1.31    setup "prem1" (style_parm_premise 1) #>
    1.32    setup "prem2" (style_parm_premise 2) #>
    1.33    setup "prem3" (style_parm_premise 3) #>