src/Pure/Proof/proof_syntax.ML
changeset 59621 291934bac95e
parent 59582 0fbed69ff081
child 60826 695cf1fab6cc
     1.1 --- a/src/Pure/Proof/proof_syntax.ML	Fri Mar 06 14:01:08 2015 +0100
     1.2 +++ b/src/Pure/Proof/proof_syntax.ML	Fri Mar 06 15:58:56 2015 +0100
     1.3 @@ -197,7 +197,7 @@
     1.4        |> add_proof_atom_consts
     1.5          (map (Long_Name.append "axm") axm_names @ map (Long_Name.append "thm") thm_names);
     1.6    in
     1.7 -    (Thm.cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
     1.8 +    (Thm.global_cterm_of thy' (term_of_proof prf), proof_of_term thy true o Thm.term_of)
     1.9    end;
    1.10  
    1.11  fun read_term thy topsort =