src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 28103 b79e61861f0f
parent 28100 7650d5e0f8fb
child 28375 c879d88d038a
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Sep 03 00:11:27 2008 +0200
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Wed Sep 03 11:09:08 2008 +0200
     1.3 @@ -296,10 +296,9 @@
     1.4  
     1.5  in
     1.6  
     1.7 -fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn (state', opt_err) =>
     1.8 +fun setup_present_hook () = Toplevel.add_hook (fn _ => fn state => fn state' =>
     1.9    if ! show_theorem_dependencies andalso
    1.10 -    can Toplevel.theory_of state andalso
    1.11 -    Toplevel.is_theory state' andalso is_none opt_err
    1.12 +    can Toplevel.theory_of state andalso Toplevel.is_theory state'
    1.13    then
    1.14      let val (names, deps) = new_thms_deps (Toplevel.theory_of state) (Toplevel.theory_of state') in
    1.15        if null names orelse null deps then ()