equal
deleted
inserted
replaced
820 (code'', del_nodes ["<Top>"] gr') |
820 (code'', del_nodes ["<Top>"] gr') |
821 end; |
821 end; |
822 |
822 |
823 val generate_code_i = gen_generate_code Sign.cert_term; |
823 val generate_code_i = gen_generate_code Sign.cert_term; |
824 val generate_code = |
824 val generate_code = |
825 gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init); |
825 gen_generate_code (Syntax.read_term o ProofContext.allow_dummies o ProofContext.init_global); |
826 |
826 |
827 |
827 |
828 (**** Reflection ****) |
828 (**** Reflection ****) |
829 |
829 |
830 val strip_tname = implode o tl o explode; |
830 val strip_tname = implode o tl o explode; |
906 |
906 |
907 val eval_result = Unsynchronized.ref (fn () => Bound 0); |
907 val eval_result = Unsynchronized.ref (fn () => Bound 0); |
908 |
908 |
909 fun eval_term thy t = |
909 fun eval_term thy t = |
910 let |
910 let |
911 val ctxt = ProofContext.init thy; |
911 val ctxt = ProofContext.init_global thy; |
912 val e = |
912 val e = |
913 let |
913 let |
914 val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse |
914 val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse |
915 error "Term to be evaluated contains type variables"; |
915 error "Term to be evaluated contains type variables"; |
916 val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse |
916 val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse |