src/Pure/Thy/term_style.ML
changeset 41686 d8efc2490b8e
parent 41685 e29ea98a76ce
child 42016 3b6826b3ed37
     1.1 --- a/src/Pure/Thy/term_style.ML	Tue Feb 01 21:09:52 2011 +0100
     1.2 +++ b/src/Pure/Thy/term_style.ML	Wed Feb 02 08:47:45 2011 +0100
     1.3 @@ -110,14 +110,12 @@
     1.4    | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
     1.5    | isub_term t = t;
     1.6  
     1.7 -val style_isub = Scan.succeed (K isub_term);
     1.8 -
     1.9  val _ = Context.>> (Context.map_theory
    1.10   (setup "lhs" (style_lhs_rhs fst) #>
    1.11    setup "rhs" (style_lhs_rhs snd) #>
    1.12    setup "prem" style_prem #>
    1.13    setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
    1.14 -  setup "isub" style_isub #>
    1.15 +  setup "isub" (Scan.succeed (K isub_term)) #>
    1.16    setup "prem1" (style_parm_premise 1) #>
    1.17    setup "prem2" (style_parm_premise 2) #>
    1.18    setup "prem3" (style_parm_premise 3) #>