src/Pure/Thy/term_style.ML
changeset 53021 d0fa3f446b9d
parent 50638 eedc01eca736
child 53171 a5e54d4d9081
     1.1 --- a/src/Pure/Thy/term_style.ML	Tue Aug 13 19:52:12 2013 +0200
     1.2 +++ b/src/Pure/Thy/term_style.ML	Tue Aug 13 20:34:46 2013 +0200
     1.3 @@ -75,27 +75,27 @@
     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 +fun sub_symbols (d :: s :: ss) =
     1.9        if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
    1.10 -      then d :: "\\<^isub>" :: isub_symbols (s :: ss)
    1.11 +      then d :: "\\<^sub>" :: sub_symbols (s :: ss)
    1.12        else d :: s :: ss
    1.13 -  | isub_symbols cs = cs;
    1.14 +  | sub_symbols cs = cs;
    1.15  
    1.16 -val isub_name = implode o rev o isub_symbols o rev o Symbol.explode;
    1.17 +val sub_name = implode o rev o sub_symbols o rev o Symbol.explode;
    1.18  
    1.19 -fun isub_term (Free (n, T)) = Free (isub_name n, T)
    1.20 -  | isub_term (Var ((n, idx), T)) =
    1.21 -      if idx <> 0 then Var ((isub_name (n ^ string_of_int idx), 0), T)
    1.22 -      else Var ((isub_name n, 0), T)
    1.23 -  | isub_term (t $ u) = isub_term t $ isub_term u
    1.24 -  | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
    1.25 -  | isub_term t = t;
    1.26 +fun sub_term (Free (n, T)) = Free (sub_name n, T)
    1.27 +  | sub_term (Var ((n, idx), T)) =
    1.28 +      if idx <> 0 then Var ((sub_name (n ^ string_of_int idx), 0), T)
    1.29 +      else Var ((sub_name n, 0), T)
    1.30 +  | sub_term (t $ u) = sub_term t $ sub_term u
    1.31 +  | sub_term (Abs (n, T, b)) = Abs (sub_name n, T, sub_term b)
    1.32 +  | sub_term t = t;
    1.33  
    1.34  val _ = Context.>> (Context.map_theory
    1.35   (setup "lhs" (style_lhs_rhs fst) #>
    1.36    setup "rhs" (style_lhs_rhs snd) #>
    1.37    setup "prem" style_prem #>
    1.38    setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
    1.39 -  setup "isub" (Scan.succeed (K isub_term))));
    1.40 +  setup "sub" (Scan.succeed (K sub_term))));
    1.41  
    1.42  end;