src/Pure/ProofGeneral/proof_general_pgip.ML
changeset 28817 c8cc94a470d4
parent 28814 463c9e9111ae
child 29349 b49d8501720a
     1.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 16 22:12:43 2008 +0100
     1.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 16 22:12:44 2008 +0100
     1.3 @@ -251,7 +251,7 @@
     1.4  local
     1.5  
     1.6  fun add_proof_body (PBody {thms, ...}) =
     1.7 -  thms |> fold (fn (_, ((name, _, _), _)) => name <> "" ? Symtab.update (name, ()));
     1.8 +  thms |> fold (fn (_, (name, _, _)) => name <> "" ? Symtab.update (name, ()));
     1.9  
    1.10  fun add_thm th =
    1.11    (case Thm.proof_body_of th of